[isabelle-dev] Duplicate theory??
Traytel Dmitriy
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.
Dmitriy
> 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.
>
> Dmitry
>
>> 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.
>>
>>
>> Makarius
>>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
More information about the isabelle-dev
mailing list