# HG changeset patch # User wenzelm # Date 952533414 -3600 # Node ID a57d72b5d272e467b4dec4350c2448f3fead83ab # Parent 61307df166bca47e4a84abce69df00a7eb86764c * isatool mkdir provides easy setup of Isabelle session directories, including proper documents; * generated LaTeX sources are now deleted after successful run (isatool document -c); may retain a copy somewhere else via -D option of isatool usedir; * old-style theories now produce (crude) LaTeX sources as well; * compression of ML heaps images may now be controlled via -c option of isabelle and isatool usedir; diff -r 61307df166bc -r a57d72b5d272 NEWS --- a/NEWS Wed Mar 08 17:35:08 2000 +0100 +++ b/NEWS Wed Mar 08 17:36:54 2000 +0100 @@ -10,6 +10,18 @@ * HOL: the constant for f``x is now "image" rather than "op ``". +*** Isabelle document preparation *** + +* isatool mkdir provides easy setup of Isabelle session directories, +including proper documents; + +* generated LaTeX sources are now deleted after successful run +(isatool document -c); may retain a copy somewhere else via -D option +of isatool usedir; + +* old-style theories now produce (crude) LaTeX sources as well; + + *** Isar *** * names of theorems etc. may be natural numbers as well; @@ -39,6 +51,12 @@ extended records as well; admit "r" as field name; +*** General *** + +* compression of ML heaps images may now be controlled via -c option +of isabelle and isatool usedir; + + New in Isabelle99 (October 1999) --------------------------------