diff -r f6fa0e526f4f -r 1e29b79db3dc NEWS
--- a/NEWS	Tue Oct 16 00:39:34 2001 +0200
+++ b/NEWS	Tue Oct 16 00:50:23 2001 +0200
@@ -21,13 +21,18 @@
 *** Isar ***
 
 * improved proof by cases and induction:
-  - divinate induct rule instantiation (excessive ?P bindings no longer required);
-  - proper enumeration of all possibilities of set/type rules (as a consequence
-    facts may be also passed through *type* rules without further ado);
+  - 'case' command admits impromptu naming of parameters (such as
+    "case (Suc n)");
+  - 'induct' method divinates rule instantiation from the inductive
+    claim; no longer requires excessive ?P bindings for proper
+    instantiation of cases;
+  - 'induct' method properly enumerates all possibilities of set/type
+    rules; as a consequence facts may be also passed through *type*
+    rules without further ado;
+  - removed obsolete "(simplified)" and "(stripped)" options of methods;
   - added 'print_induct_rules' (covered by help item in Proof General > 3.3);
-  - moved induct/cases attributes to Pure;
-  - generic setup instantiated for FOL and HOL;
-  - removed obsolete "(simplified)" and "(stripped)" options of methods;
+  - moved induct/cases attributes to Pure, methods to Provers;
+  - generic method setup instantiated for FOL and HOL;
 
 * Pure: renamed "antecedent" case to "rule_context";
 
@@ -43,7 +48,7 @@
 * HOL: 'inductive' now longer features separate (collective)
 attributes for 'intros';
 
-* HOL: canonical 'cases'/'induct' rules for n-tuples (n=3..7)
+* HOL: canonical cases/induct rules for n-tuples (n = 3..7);
 
 
 *** HOL ***