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 <[email protected]> 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 <[email protected]> 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 > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
