# HG changeset patch
# User wenzelm
# Date 959695219 -7200
# Node ID 803533fbb3ec5d6eb11f38c55cb5b9f7737e493a
# Parent  cbfebff56cc0f7935ac6fe3f6a80ec577d6eec92
* ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
timing flag supersedes proof_timing and Toplevel.trace;

diff -r cbfebff56cc0 -r 803533fbb3ec NEWS
--- 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):