# HG changeset patch
# User wenzelm
# Date 1003185574 -7200
# Node ID f6fa0e526f4f785b85a45795a4209451df4bf33e
# Parent  12a0fb3ac3664c57576a8b206f056320ab96a8bd
improved induct;

diff -r 12a0fb3ac366 -r f6fa0e526f4f NEWS
--- a/NEWS	Tue Oct 16 00:35:30 2001 +0200
+++ b/NEWS	Tue Oct 16 00:39:34 2001 +0200
@@ -21,10 +21,13 @@
 *** Isar ***
 
 * improved proof by cases and induction:
-  - moved induct/cases attributes to Pure;
+  - 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);
   - 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;
+  - removed obsolete "(simplified)" and "(stripped)" options of methods;
 
 * Pure: renamed "antecedent" case to "rule_context";