* ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
timing flag supersedes proof_timing and Toplevel.trace;

--- 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):