[isabelle-dev] Duplicate theory??

Lawrence Paulson lp15 at cam.ac.uk
Mon Apr 8 12:11:35 CEST 2019


> 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




More information about the isabelle-dev mailing list