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
