NEWS
changeset 12405 9b16f99fd7b9
parent 12364 108cdda23ab3
child 12457 cbfc53e45476
     1.1 --- a/NEWS	Thu Dec 06 00:43:03 2001 +0100
     1.2 +++ b/NEWS	Thu Dec 06 00:45:04 2001 +0100
     1.3 @@ -109,6 +109,14 @@
     1.4  * Pure: "sorry" no longer requires quick_and_dirty in interactive
     1.5  mode;
     1.6  
     1.7 +* Pure/obtain: the formal conclusion "thesis", being marked as
     1.8 +``internal'', may no longer be reference directly in the text;
     1.9 +potential INCOMPATIBILITY, may need to use "?thesis" in rare
    1.10 +situations;
    1.11 +
    1.12 +* Pure: generic 'sym' attribute which declares a rule both as pure
    1.13 +'elim?' and for the 'symmetric' operation;
    1.14 +
    1.15  * Pure/Provers/classical: simplified integration with pure rule
    1.16  attributes and methods; the classical "intro?/elim?/dest?"
    1.17  declarations coincide with the pure ones; the "rule" method no longer
    1.18 @@ -117,6 +125,9 @@
    1.19  AddXIs/AddXEs/AddXDs; all of this has some potential for
    1.20  INCOMPATIBILITY;
    1.21  
    1.22 +* Provers/classical: attribute 'swapped' produces classical inversions
    1.23 +of introduction rules;
    1.24 +
    1.25  * Provers/simplifier: 'simplified' attribute may refer to explicit
    1.26  rules instead of full simplifier context; 'iff' attribute handles
    1.27  conditional rules;
    1.28 @@ -129,6 +140,9 @@
    1.29  * HOL: 'inductive' no longer features separate (collective) attributes
    1.30  for 'intros' (was found too confusing);
    1.31  
    1.32 +* HOL: properly declared induction rules less_induct and
    1.33 +wf_induct_rule;
    1.34 +
    1.35  * HOLCF: domain package adapted to new-style theories, e.g. see
    1.36  HOLCF/ex/Dnat.thy;
    1.37