1.1 --- a/NEWS	Tue Oct 16 00:35:30 2001 +0200
     1.2 +++ b/NEWS	Tue Oct 16 00:39:34 2001 +0200
     1.3 @@ -21,10 +21,13 @@
     1.4  *** Isar ***
     1.5  
     1.6  * improved proof by cases and induction:
     1.7 +  - divinate induct rule instantiation (excessive ?P bindings no longer required);
     1.8 +  - proper enumeration of all possibilities of set/type rules (as a consequence
     1.9 +    facts may be also passed through *type* rules without further ado);
    1.10 +  - added 'print_induct_rules' (covered by help item in Proof General > 3.3);
    1.11    - moved induct/cases attributes to Pure;
    1.12 -  - added 'print_induct_rules' (covered by help item in Proof General > 3.3);
    1.13    - generic setup instantiated for FOL and HOL;
    1.14 -  - removed obsolete "(simplified)" and "(stripped)" options;
    1.15 +  - removed obsolete "(simplified)" and "(stripped)" options of methods;
    1.16  
    1.17  * Pure: renamed "antecedent" case to "rule_context";
    1.18