diff -r b0ad1ed24cf6 -r efaba354b7f1 NEWS
--- a/NEWS	Thu Nov 30 17:55:17 2000 +0100
+++ b/NEWS	Thu Nov 30 20:03:39 2000 +0100
@@ -32,6 +32,12 @@
 
 *** Isar ***
 
+* Pure: Isar now suffers initial goal statements to contain unbound
+schematic variables (this does not conform to actual readable proof
+documents, due to unpredictable outcome and non-compositional proof
+checking); users who know what they are doing may use schematic goals
+for Prolog-style synthesis of proven results;
+
 * Pure: assumption method (an implicit finishing) now handles actual
 rules as well;
 
@@ -49,6 +55,10 @@
 * HOL: improved method 'induct' --- now handles non-atomic goals
 (potential INCOMPATIBILITY); tuned error handling;
 
+* HOL: cases and induct rules may now provide explicit hint about the
+number of facts to be consumed (0 for "type" and 1 for "set" rules);
+any remaining facts are inserted into the goal verbatim;
+
 
 *** HOL ***
 
@@ -67,14 +77,20 @@
 
 *** CTT ***
 
-* CTT: x-symbol support for Pi, Sigma, -->, : (membership)
-  note that "lam" is displayed as TWO lambda-symbols
+* CTT: x-symbol support for Pi, Sigma, -->, : (membership); note that
+"lam" is displayed as TWO lambda-symbols
 
-* CTT: theory Main now available, containing everything
-(that is, Bool and Arith) 
+* CTT: theory Main now available, containing everything (that is, Bool
+and Arith);
+
 
 *** General ***
 
+* Pure: the Simplifier has been implemented properly as a derived rule
+outside of the actual kernel (at last!); the overall performance
+penalty in practical applications is about 50%, while reliability of
+the Isabelle inference kernel has been greatly improved;
+
 * Provers: fast_tac (and friends) now handle actual object-logic rules
 as assumptions as well;