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