- 'induct' method now derives symbolic cases from the *rulified* rule
authorwenzelm
Tue Oct 30 17:33:56 2001 +0100 (2001-10-30)
changeset 1198626b95a6f3f79
parent 11985 06658189cd51
child 11987 bf31b35949ce
- 'induct' method now derives symbolic cases from the *rulified* rule
(before it used to rulify cases stemming from the internal atomized
version); this means that the context of a non-atomic statement
becomes is included in the hypothesis, avoiding the slightly
cumbersome show "PROP ?case" form;
NEWS
     1.1 --- a/NEWS	Tue Oct 30 17:33:03 2001 +0100
     1.2 +++ b/NEWS	Tue Oct 30 17:33:56 2001 +0100
     1.3 @@ -33,14 +33,24 @@
     1.4  *** Isar ***
     1.5  
     1.6  * improved proof by cases and induction:
     1.7 +
     1.8    - 'case' command admits impromptu naming of parameters (such as
     1.9 -    "case (Suc n)");
    1.10 +"case (Suc n)");
    1.11 +
    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 +claim; no longer requires excessive ?P bindings for proper
    1.16 +instantiation of cases;
    1.17 +
    1.18    - 'induct' method properly enumerates all possibilities of set/type
    1.19 -    rules; as a consequence facts may be also passed through *type*
    1.20 -    rules without further ado;
    1.21 +rules; as a consequence facts may be also passed through *type* rules
    1.22 +without further ado;
    1.23 +
    1.24 +  - 'induct' method now derives symbolic cases from the *rulified*
    1.25 +rule (before it used to rulify cases stemming from the internal
    1.26 +atomized version); this means that the context of a non-atomic
    1.27 +statement becomes is included in the hypothesis, avoiding the slightly
    1.28 +cumbersome show "PROP ?case" form;
    1.29 +
    1.30    - removed obsolete "(simplified)" and "(stripped)" options of methods;
    1.31    - added 'print_induct_rules' (covered by help item in Proof General > 3.3);
    1.32    - moved induct/cases attributes to Pure, methods to Provers;