[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Fri Jun 27 23:47:18 CEST 2014
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.
More information about the isabelle-dev