NEWS
changeset 56279 b4d874f6c6be
parent 56276 9e2d5e3debd3
child 56281 03c3d1a7c3b8
     1.1 --- a/NEWS	Tue Mar 25 16:11:00 2014 +0100
     1.2 +++ b/NEWS	Tue Mar 25 16:54:38 2014 +0100
     1.3 @@ -34,10 +34,6 @@
     1.4  exception.  Potential INCOMPATIBILITY for non-conformant tactical
     1.5  proof tools.
     1.6  
     1.7 -* Discontinued old Toplevel.debug in favour of system option
     1.8 -"exception_trace", which may be also declared within the context via
     1.9 -"declare [[exception_trace = true]]".  Minor INCOMPATIBILITY.
    1.10 -
    1.11  * Command 'SML_file' reads and evaluates the given Standard ML file.
    1.12  Toplevel bindings are stored within the theory context; the initial
    1.13  environment is restricted to the Standard ML implementation of
    1.14 @@ -545,6 +541,13 @@
    1.15  
    1.16  *** ML ***
    1.17  
    1.18 +* Discontinued old Toplevel.debug in favour of system option
    1.19 +"ML_exception_trace", which may be also declared within the context via
    1.20 +"declare [[ML_exception_trace = true]]".  Minor INCOMPATIBILITY.
    1.21 +
    1.22 +* Renamed option "ML_trace" to "ML_source_trace". Minor
    1.23 +INCOMPATIBILITY.
    1.24 +
    1.25  * Proper context discipline for read_instantiate and instantiate_tac:
    1.26  variables that are meant to become schematic need to be given as
    1.27  fixed, and are generalized by the explicit context of local variables.