equal
deleted
inserted
replaced
227 |
227 |
228 * compression of ML heaps images may now be controlled via -c option |
228 * compression of ML heaps images may now be controlled via -c option |
229 of isabelle and isatool usedir (currently only observed by Poly/ML); |
229 of isabelle and isatool usedir (currently only observed by Poly/ML); |
230 |
230 |
231 * provide TAGS file for Isabelle sources; |
231 * provide TAGS file for Isabelle sources; |
|
232 |
|
233 * ML: infix 'OF' is a version of 'MRS' with more appropriate argument |
|
234 order; |
232 |
235 |
233 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global |
236 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global |
234 timing flag supersedes proof_timing and Toplevel.trace; |
237 timing flag supersedes proof_timing and Toplevel.trace; |
235 |
238 |
236 * ML: new combinators |>> and |>>> for incremental transformations |
239 * ML: new combinators |>> and |>>> for incremental transformations |