[isabelle-dev] Remaining uses of Proof General?

Makarius 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 mailing list