equal
deleted
inserted
replaced
103 |
103 |
104 * browser info session directories are now self-contained (may be put |
104 * browser info session directories are now self-contained (may be put |
105 on WWW server seperately); improved graphs of nested sessions; removed |
105 on WWW server seperately); improved graphs of nested sessions; removed |
106 graph for 'all sessions'; |
106 graph for 'all sessions'; |
107 |
107 |
108 * several improvements in isabelle.sty; \isamarkupheader is now |
108 * several improvements in isabelle.sty; \isabellestyle{it} produces |
109 \section by default; |
109 near math mode output; \isamarkupheader is now \section by default; |
110 |
110 |
111 |
111 |
112 *** Isar *** |
112 *** Isar *** |
113 |
113 |
114 * Pure: local results and corresponding term bindings are now subject |
114 * Pure: local results and corresponding term bindings are now subject |
323 |
323 |
324 * compression of ML heaps images may now be controlled via -c option |
324 * compression of ML heaps images may now be controlled via -c option |
325 of isabelle and isatool usedir (currently only observed by Poly/ML); |
325 of isabelle and isatool usedir (currently only observed by Poly/ML); |
326 |
326 |
327 * provide TAGS file for Isabelle sources; |
327 * provide TAGS file for Isabelle sources; |
|
328 |
|
329 * settings: smart setup of canonical ML_HOME, ISABELLE_INTERFACE, and |
|
330 XSYMBOL_HOME; no longer need to do manual configuration in most |
|
331 situations; |
328 |
332 |
329 * ML: infix 'OF' is a version of 'MRS' with more appropriate argument |
333 * ML: infix 'OF' is a version of 'MRS' with more appropriate argument |
330 order; |
334 order; |
331 |
335 |
332 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global |
336 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global |