And I wonder whether the problem is that
Cardinals/Wellorder_Constructions
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.
Larry
> On 4 Apr 2019, at 15:37, Lawrence Paulson <[email protected]> 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"
> imports
> Product_Groups
> "HOL-Cardinals.Cardinal_Arithmetic"
> "HOL-Library.Countable_Set" "HOL-Library.Poly_Mapping"
> "HOL-Library.Equipollence”
>
> But any attempt to load it produces the error message
>
>> /Users/lp15/isabelle/Repos/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
>> 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?
> Larry
>
>
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
