[isabelle-dev] NEWS: command 'ML_export'
makarius at sketis.net
Fri May 25 23:32:10 CEST 2018
*** ML ***
* Command 'ML_export' exports ML toplevel bindings to the global
bootstrap environment of the ML process. This allows ML evaluation
without a formal theory context, e.g. in command-line tools like
This refers to Isabelle/cbee43ff4ceb.
Here are also the examples from the "system" manual in
isabelle process -e 'Command_Line.tool0 (fn () => writeln "OK")'
isabelle process -e 'Command_Line.tool0 (fn () => error "Bad")'
In other words, it is now quite easy to produce clean command-line
tools, based on ML functions inside a regular Isabelle session.
More information about the isabelle-dev