[isabelle-dev] Duplicate theory??

Lawrence Paulson lp15 at cam.ac.uk
Thu Apr 4 16:37:22 CEST 2019

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

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

More information about the isabelle-dev mailing list