1.1 --- a/NEWS	Wed Oct 31 01:26:42 2001 +0100
     1.2 +++ b/NEWS	Wed Oct 31 01:27:04 2001 +0100
     1.3 @@ -33,6 +33,10 @@
     1.4  *** Isar ***
     1.5  
     1.6  * improved proof by cases and induction:
     1.7 +  - removed obsolete "(simplified)" and "(stripped)" options of methods;
     1.8 +  - added 'print_induct_rules' (covered by help item in Proof General > 3.3);
     1.9 +  - moved induct/cases attributes to Pure, methods to Provers;
    1.10 +  - generic method setup instantiated for FOL and HOL;
    1.11  
    1.12    - 'case' command admits impromptu naming of parameters (such as
    1.13  "case (Suc n)");
    1.14 @@ -51,10 +55,12 @@
    1.15  statement becomes is included in the hypothesis, avoiding the slightly
    1.16  cumbersome show "PROP ?case" form;
    1.17  
    1.18 -  - removed obsolete "(simplified)" and "(stripped)" options of methods;
    1.19 -  - added 'print_induct_rules' (covered by help item in Proof General > 3.3);
    1.20 -  - moved induct/cases attributes to Pure, methods to Provers;
    1.21 -  - generic method setup instantiated for FOL and HOL;
    1.22 +  - 'induct' may now use elim-style induction rules without chaining
    1.23 +facts, using ``missing'' premises from the goal state; this allows
    1.24 +rules stemming from inductive sets to be applied in unstructured
    1.25 +scripts, while still benefitting from proper handling of non-atomic
    1.26 +statements; NB: major inductive premises need to be put first, all the
    1.27 +rest of the goal is passed through the induction;
    1.28  
    1.29  * Pure: renamed "antecedent" case to "rule_context";
    1.30