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-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
