tuned;
authorwenzelm
Tue Oct 16 00:50:23 2001 +0200 (2001-10-16)
changeset 117971e29b79db3dc
parent 11796 f6fa0e526f4f
child 11798 fbab70de9b0d
tuned;
NEWS
     1.1 --- a/NEWS	Tue Oct 16 00:39:34 2001 +0200
     1.2 +++ b/NEWS	Tue Oct 16 00:50:23 2001 +0200
     1.3 @@ -21,13 +21,18 @@
     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 +  - 'case' command admits impromptu naming of parameters (such as
    1.11 +    "case (Suc n)");
    1.12 +  - 'induct' method divinates rule instantiation from the inductive
    1.13 +    claim; no longer requires excessive ?P bindings for proper
    1.14 +    instantiation of cases;
    1.15 +  - 'induct' method properly enumerates all possibilities of set/type
    1.16 +    rules; as a consequence facts may be also passed through *type*
    1.17 +    rules without further ado;
    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;
    1.21 -  - generic setup instantiated for FOL and HOL;
    1.22 -  - removed obsolete "(simplified)" and "(stripped)" options of methods;
    1.23 +  - moved induct/cases attributes to Pure, methods to Provers;
    1.24 +  - generic method setup instantiated for FOL and HOL;
    1.25  
    1.26  * Pure: renamed "antecedent" case to "rule_context";
    1.27  
    1.28 @@ -43,7 +48,7 @@
    1.29  * HOL: 'inductive' now longer features separate (collective)
    1.30  attributes for 'intros';
    1.31  
    1.32 -* HOL: canonical 'cases'/'induct' rules for n-tuples (n=3..7)
    1.33 +* HOL: canonical cases/induct rules for n-tuples (n = 3..7);
    1.34  
    1.35  
    1.36  *** HOL ***