NEWS
changeset 56275 600f432ab556
parent 56265 785569927666
child 56276 9e2d5e3debd3
     1.1 --- a/NEWS	Tue Mar 25 10:37:10 2014 +0100
     1.2 +++ b/NEWS	Tue Mar 25 13:18:10 2014 +0100
     1.3 @@ -38,6 +38,11 @@
     1.4  "exception_trace", which may be also declared within the context via
     1.5  "declare [[exception_trace = true]]".  Minor INCOMPATIBILITY.
     1.6  
     1.7 +* Command 'SML_file' reads and evaluates the given Standard ML file.
     1.8 +Toplevel bindings are stored within the theory context; the initial
     1.9 +environment is restricted to the Standard ML implementation of
    1.10 +Poly/ML, without the add-ons of Isabelle/ML.
    1.11 +
    1.12  
    1.13  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.14