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
