> On 8 Apr 2019, at 12:11, Lawrence Paulson <[email protected]> wrote: > >> On 7 Apr 2019, at 20:08, Traytel Dmitriy <[email protected]> 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). Dmitriy _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
