[isabelle-dev] Duplicate theory??

Traytel Dmitriy traytel at inf.ethz.ch
Mon Apr 8 12:21:06 CEST 2019

> On 8 Apr 2019, at 12:11, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
>> On 7 Apr 2019, at 20:08, Traytel Dmitriy <traytel at inf.ethz.ch> wrote:
>> In 3a1b2d8c89aa, there is now a bundle cardinal_syntax (and the theory Cardinal_Notations is gone). HOL-Cardinals does not depend on HOL-Library anymore.
> Thanks. But now nothing works. I get
>> /Users/lp15/isabelle/Repos/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
>> Cannot start: 
>> *** Duplicate theory "/Users/lp15/isabelle/Repos/src/HOL/Library/Countable_Set_Type.thy" vs. "HOL-Library.Countable_Set_Type"
> 36821db2e356+ tip

What is the invocation of Isabelle that leads to this? Do you have some local root files?

I have tested as usual with

isabelle build -a

(which succeeded).


More information about the isabelle-dev mailing list