--- a/NEWS Thu Mar 16 00:29:03 2000 +0100
+++ b/NEWS Thu Mar 16 00:31:58 2000 +0100
@@ -14,7 +14,7 @@
* ML: PureThy.add_thms/add_axioms/add_defs now return theorems;
-*** Isabelle document preparation ***
+*** Document preparation ***
* isatool mkdir provides easy setup of Isabelle session directories,
including proper documents;
@@ -35,11 +35,15 @@
* Pure: new 'obtain' language element supports generalized existence
proofs;
-* Pure: much better support for case-analysis type proofs: new 'case'
+* Pure: scalable support for case-analysis type proofs: new 'case'
language element refers to local contexts symbolically, as produced by
certain proof methods; internally, case names are attached to theorems
as "tags";
+* Provers: splitter support (via 'split' attribute and 'simp' method
+modifier); 'simp' method: 'only:' modifier removes loopers as well
+(including splits);
+
* HOL: new proof method 'cases' and improved version of 'induct' now
support named cases; major packages (inductive, datatype, primrec,
recdef) support case names and properly name parameters;
@@ -51,6 +55,12 @@
* intro/elim/dest attributes: changed ! / !! flags to ? / ??;
+* 'pr' command: optional goals_limit argument;
+
+* diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit
+additional print modes to be specified; e.g. pr(latex) will print
+proof according to the Isabelle LaTeX style;
+
*** HOL ***