--- a/NEWS Tue Mar 25 16:11:00 2014 +0100
+++ b/NEWS Tue Mar 25 16:54:38 2014 +0100
@@ -34,10 +34,6 @@
exception. Potential INCOMPATIBILITY for non-conformant tactical
proof tools.
-* Discontinued old Toplevel.debug in favour of system option
-"exception_trace", which may be also declared within the context via
-"declare [[exception_trace = true]]". Minor INCOMPATIBILITY.
-
* Command 'SML_file' reads and evaluates the given Standard ML file.
Toplevel bindings are stored within the theory context; the initial
environment is restricted to the Standard ML implementation of
@@ -545,6 +541,13 @@
*** ML ***
+* Discontinued old Toplevel.debug in favour of system option
+"ML_exception_trace", which may be also declared within the context via
+"declare [[ML_exception_trace = true]]". Minor INCOMPATIBILITY.
+
+* Renamed option "ML_trace" to "ML_source_trace". Minor
+INCOMPATIBILITY.
+
* Proper context discipline for read_instantiate and instantiate_tac:
variables that are meant to become schematic need to be given as
fixed, and are generalized by the explicit context of local variables.