NEWS
changeset 9052 7db48fe85b05
parent 9028 8a1ec8f05f14
child 9057 af1ca1acf292
equal deleted inserted replaced
9051:887a15590f0e 9052:7db48fe85b05
   198 * improved name spaces: ambiguous output is qualified; support for
   198 * improved name spaces: ambiguous output is qualified; support for
   199 hiding of names;
   199 hiding of names;
   200 
   200 
   201 * compression of ML heaps images may now be controlled via -c option
   201 * compression of ML heaps images may now be controlled via -c option
   202 of isabelle and isatool usedir (currently only observed by Poly/ML);
   202 of isabelle and isatool usedir (currently only observed by Poly/ML);
       
   203 
       
   204 * provide TAGS file for Isabelle sources;
   203 
   205 
   204 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
   206 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
   205 timing flag supersedes proof_timing and Toplevel.trace;
   207 timing flag supersedes proof_timing and Toplevel.trace;
   206 
   208 
   207 * ML: new combinators |>> and |>>> for incremental transformations
   209 * ML: new combinators |>> and |>>> for incremental transformations