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