NEWS
changeset 56618 874bdedb2313
parent 56598 2cc2cb56cbdd
child 56652 b0126a5a256d
     1.1 --- a/NEWS	Thu Apr 17 14:52:23 2014 +0200
     1.2 +++ b/NEWS	Sat Apr 19 17:23:05 2014 +0200
     1.3 @@ -37,11 +37,14 @@
     1.4  exception.  Potential INCOMPATIBILITY for non-conformant tactical
     1.5  proof tools.
     1.6  
     1.7 -* Command 'SML_file' reads and evaluates the given Standard ML file.
     1.8 +* Support for official Standard ML within the Isabelle context.
     1.9 +Command 'SML_file' reads and evaluates the given Standard ML file.
    1.10  Toplevel bindings are stored within the theory context; the initial
    1.11  environment is restricted to the Standard ML implementation of
    1.12 -Poly/ML, without the add-ons of Isabelle/ML.  See also
    1.13 -~~/src/Tools/SML/Examples.thy for some basic examples.
    1.14 +Poly/ML, without the add-ons of Isabelle/ML.  Commands 'SML_import'
    1.15 +and 'SML_export' allow to exchange toplevel bindings between the two
    1.16 +separate environments.  See also ~~/src/Tools/SML/Examples.thy for
    1.17 +some examples.
    1.18  
    1.19  
    1.20  *** Prover IDE -- Isabelle/Scala/jEdit ***