[isabelle-dev] Duplicate theory??

[Traytel Dmitriy]

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