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