[isabelle-dev] Duplicate theory??
lp15 at cam.ac.uk
Thu Apr 4 17:29:47 CEST 2019
And I wonder whether the problem is that
imports "HOL-Library.Cardinal_Notations" (Which is a tiny file) which might create a circular dependence if any theory in Library tried to load something from Cardinals. Not that I understand how sessions work.
> On 4 Apr 2019, at 15:37, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> I’m trying to install some material in time for the next release and I've got tangled up in some issue connected with session structure. The theory header looks like this:
> theory "Free_Abelian_Groups"
> "HOL-Library.Countable_Set" "HOL-Library.Poly_Mapping" "HOL-Library.Equipollence”
> But any attempt to load it produces the error message
>> Cannot start:
>> *** Duplicate theory "HOL-Cardinals.Cardinal_Arithmetic" vs. "/Users/lp15/isabelle/Repos/src/HOL/Cardinals/Cardinal_Arithmetic.thy”
> I note that absolutely nothing in the distribution imports HOL-Cardinals. However, it’s imported in a number of places in the AFP. What gives?
More information about the isabelle-dev