NEWS
changeset 9941 fe05af7ec816
parent 9937 431c96ac997e
child 9971 e0164f01d55a
     1.1 --- a/NEWS	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/NEWS	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -52,8 +52,8 @@
     1.4  
     1.5  * ZF: new treatment of arithmetic (nat & int) may break some old proofs;
     1.6  
     1.7 -* Isar/Provers: intro/elim/dest attributes: changed
     1.8 -intro/intro!/intro!!  flags to intro!/intro/intro? (in most cases, one
     1.9 +* Isar/Provers: intro/elim/dest attributes changed; renamed
    1.10 +intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one
    1.11  should have to change intro!! to intro? only); replaced "delrule" by
    1.12  "rule del";
    1.13  
    1.14 @@ -61,7 +61,7 @@
    1.15  
    1.16  * Isar: renamed 'RS' attribute to 'THEN';
    1.17  
    1.18 -* Isar: renamed some attributes (rulify -> rulified, elimify -> elimified, ...);
    1.19 +* Isar: renamed some attributes (rulify -> rule_format, elimify -> elim_format, ...);
    1.20  
    1.21  * Isar/HOL: renamed "intrs" to "intros" in inductive definitions;
    1.22  
    1.23 @@ -192,9 +192,10 @@
    1.24  'inductive_cases' command and 'ind_cases' method; NOTE: use (cases
    1.25  (simplified)) method in proper proofs;
    1.26  
    1.27 -* Provers: intro/elim/dest attributes: changed intro/intro!/intro!!
    1.28 -flags to intro!/intro/intro? (in most cases, one should have to change
    1.29 -intro!! to intro? only); replaced "delrule" by "rule del";
    1.30 +* Provers: intro/elim/dest attributes changed; renamed
    1.31 +intro/intro!/intro!! flags to intro!/intro/intro? (INCOMPATIBILITY, in
    1.32 +most cases, one should have to change intro!! to intro? only);
    1.33 +replaced "delrule" by "rule del";
    1.34  
    1.35  * names of theorems etc. may be natural numbers as well;
    1.36  
    1.37 @@ -336,6 +337,9 @@
    1.38  
    1.39  *** General ***
    1.40  
    1.41 +* Provers: delrules now handles destruct rules as well (no longer need
    1.42 +explicit make_elim);
    1.43 +
    1.44  * Provers: blast(_tac) now handles actual object-logic rules as
    1.45  assumptions; note that auto(_tac) uses blast(_tac) internally as well;
    1.46