--- 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";