--- a/NEWS Sun May 28 21:58:29 2000 +0200
+++ b/NEWS Tue May 30 16:00:19 2000 +0200
@@ -40,6 +40,9 @@
* Isar: changed syntax of local blocks from {{ }} to { };
+* ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
+timing flag supersedes proof_timing and Toplevel.trace;
+
* ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
* LaTeX: several improvements of isabelle.sty;
@@ -193,6 +196,9 @@
* compression of ML heaps images may now be controlled via -c option
of isabelle and isatool usedir (currently only observed by Poly/ML);
+* ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
+timing flag supersedes proof_timing and Toplevel.trace;
+
* ML: new combinators |>> and |>>> for incremental transformations
with secondary results (e.g. certain theory extensions):