* Pure/Provers/classical: simplified integration with pure rule
authorwenzelm
Wed Dec 05 02:58:04 2001 +0100 (2001-12-05)
changeset 12364108cdda23ab3
parent 12363 a1784e56d8d6
child 12365 a90156701dad
* Pure/Provers/classical: simplified integration with pure rule
attributes and methods;
NEWS
     1.1 --- a/NEWS	Tue Dec 04 19:53:55 2001 +0100
     1.2 +++ b/NEWS	Wed Dec 05 02:58:04 2001 +0100
     1.3 @@ -109,8 +109,17 @@
     1.4  * Pure: "sorry" no longer requires quick_and_dirty in interactive
     1.5  mode;
     1.6  
     1.7 -* Provers: 'simplified' attribute may refer to explicit rules instead
     1.8 -of full simplifier context; 'iff' attribute handles conditional rules;
     1.9 +* Pure/Provers/classical: simplified integration with pure rule
    1.10 +attributes and methods; the classical "intro?/elim?/dest?"
    1.11 +declarations coincide with the pure ones; the "rule" method no longer
    1.12 +includes classically swapped intros; "intro" and "elim" methods no
    1.13 +longer pick rules from the context; also got rid of ML declarations
    1.14 +AddXIs/AddXEs/AddXDs; all of this has some potential for
    1.15 +INCOMPATIBILITY;
    1.16 +
    1.17 +* Provers/simplifier: 'simplified' attribute may refer to explicit
    1.18 +rules instead of full simplifier context; 'iff' attribute handles
    1.19 +conditional rules;
    1.20  
    1.21  * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
    1.22  
    1.23 @@ -144,8 +153,8 @@
    1.24    - type nat has special constructor Suc, and generally prefers Suc 0
    1.25    over 1::nat and Suc (Suc 0) over 2::nat;
    1.26  
    1.27 -This change may cause significant INCOMPATIBILITIES; here are some
    1.28 -hints on converting existing sources:
    1.29 +This change may cause significant problems of INCOMPATIBILITY; here
    1.30 +are some hints on converting existing sources:
    1.31  
    1.32    - due to the new "num" token, "-0" and "-1" etc. are now atomic
    1.33    entities, so expressions involving "-" (unary or binary minus) need