tuned;
authorwenzelm
Thu Dec 07 22:35:25 2000 +0100 (2000-12-07)
changeset 10634b4c3af8ebada
parent 10633 85c5645a8a93
child 10635 b115460e5c50
tuned;
NEWS
     1.1 --- a/NEWS	Thu Dec 07 22:27:57 2000 +0100
     1.2 +++ b/NEWS	Thu Dec 07 22:35:25 2000 +0100
     1.3 @@ -4,7 +4,8 @@
     1.4  
     1.5  *** Overview of INCOMPATIBILITIES ***
     1.6  
     1.7 -* HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function;
     1.8 +* HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse"
     1.9 +function;
    1.10  
    1.11  * HOL: induct renamed to lfp_induct;
    1.12  
    1.13 @@ -26,10 +27,10 @@
    1.14  * support sub/super scripts (for single symbols only), input syntax is
    1.15  like this: "A\<^sup>*" or "A\<^sup>\<star>";
    1.16  
    1.17 -* antiquotation @{goals} and @{subgoals} for output of *dynamic* goals state;
    1.18 -Note that presentation of goal states does not conform to actual
    1.19 -human-readable proof documents.  Please do not include goal states
    1.20 -into document output unless you really know what you are doing!
    1.21 +* antiquotation @{goals} and @{subgoals} for output of *dynamic* goals
    1.22 +state; Note that presentation of goal states does not conform to
    1.23 +actual human-readable proof documents.  Please do not include goal
    1.24 +states into document output unless you really know what you are doing!
    1.25  
    1.26  
    1.27  *** Isar ***
    1.28 @@ -88,6 +89,8 @@
    1.29  
    1.30  *** General ***
    1.31  
    1.32 +* system: support Poly/ML 4.0 (current beta versions);
    1.33 +
    1.34  * Pure: the Simplifier has been implemented properly as a derived rule
    1.35  outside of the actual kernel (at last!); the overall performance
    1.36  penalty in practical applications is about 50%, while reliability of