NEWS
changeset 68276 cbee43ff4ceb
parent 68260 61188c781cdd
child 68292 7ca0c23179e6
--- a/NEWS	Fri May 25 22:47:36 2018 +0200
+++ b/NEWS	Fri May 25 22:47:57 2018 +0200
@@ -358,6 +358,11 @@
 * Operation Export.export emits theory exports (arbitrary blobs), which
 are stored persistently in the session build database.
 
+* 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".
+
 
 *** System ***