[isabelle-dev] Duplicate theory??
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
> Cannot start:
> *** Duplicate theory "/Users/lp15/isabelle/Repos/src/HOL/Library/Countable_Set_Type.thy" vs. "HOL-Library.Countable_Set_Type"
More information about the isabelle-dev