[isabelle-dev] Duplicate theory??

Makarius makarius at sketis.net
Fri Apr 5 16:50:20 CEST 2019

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.


More information about the isabelle-dev mailing list