# HG changeset patch
# User wenzelm
# Date 953163118 -3600
# Node ID 5f3b0e02ec153b33a204778423e45ebae20d475a
# Parent  85f504900ed5e9eb98fcd05abd8322ca305fd8be
Isar: splitter support; improved diagnostics;
tuned;

diff -r 85f504900ed5 -r 5f3b0e02ec15 NEWS
--- 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 ***