On Fri, 27 Jun 2014, Peter Lammich wrote:
* Writing tools in ML (ML-blocks in thy-file)
Just a side remark: in the repository version we are talking about, and
thus the coming release, ML in auxiliary files works smoothly and often
better than the ML blocks, because the file gets its own ML mode.
There is nothing wrong about ML blocks, just an equal balance between 'ML'
and 'ML_file' to choose whatever fits best the size of the ML code module.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
