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 ***