[isabelle-dev] Duplicate theory??
traytel at inf.ethz.ch
Sun Apr 7 21:08:24 CEST 2019
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.
> On 5 Apr 2019, at 17:54, Traytel Dmitriy <traytel at inf.ethz.ch> wrote:
> Indeed, a bundle is probably the best approach. I'll look into this once my Isabelle builds again.
>> On 5 Apr 2019, at 16:50, Makarius <makarius at sketis.net> wrote:
>> On 05/04/2019 16:48, Lawrence Paulson wrote:
>>> Can I leave this with you then?
>>> Let me know if you are successful. Perhaps this tiny theory could be eliminated altogether. What is the point of defining the syntax separate from the semantics?
>> You can try to make this a bundle, to get more modular ways to
>> enable/disable the syntax locally.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev