[isabelle-dev] Duplicate theory??
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
>> 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
More information about the isabelle-dev