1.1 --- a/NEWS	Thu Oct 04 16:07:20 2001 +0200
     1.2 +++ b/NEWS	Thu Oct 04 16:07:43 2001 +0200
     1.3 @@ -16,17 +16,20 @@
     1.4  
     1.5  *** Isar ***
     1.6  
     1.7 -* Isar/Pure: renamed "antecedent" case to "rule_context";
     1.8 -
     1.9 -* Isar/HOL: 'recdef' now fails on unfinished automated proofs, use
    1.10 +* renamed "antecedent" case to "rule_context";
    1.11 +
    1.12 +* improved proof by cases and induction:
    1.13 +  - moved induct/cases attributes to Pure;
    1.14 +  - added 'print_induct_rules' (covered by help item in Proof General > 3.3);
    1.15 +  - generic setup instantiated for FOL and HOL;
    1.16 +  - removed obsolete "(simplified)" and "(stripped)" options;
    1.17 +
    1.18 +* HOL: 'recdef' now fails on unfinished automated proofs, use
    1.19  "(permissive)" option to recover old behavior;
    1.20  
    1.21 -* Isar/HOL: 'inductive' now longer features separate (collective)
    1.22 +* HOL: 'inductive' now longer features separate (collective)
    1.23  attributes for 'intros';
    1.24  
    1.25 -* moved induct/cases attributes to Pure, added 'print_induct_rules'
    1.26 -command;
    1.27 -
    1.28  
    1.29  *** HOL ***
    1.30