*** 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 "isabelle process".
This refers to Isabelle/cbee43ff4ceb. Here are also the examples from the "system" manual in Isabelle/b5d0318757f0: 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. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev