[isabelle-dev] Duplicate theory??

Lawrence Paulson 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"
>  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

More information about the isabelle-dev mailing list