[isabelle-dev] Duplicate theory??

[Lawrence Paulson]

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 <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
> 
>