tuned;
authorwenzelm
Sun Feb 11 13:26:23 2001 +0100 (2001-02-11)
changeset 11094b803ef642e60
parent 11093 62c2e0af1d30
child 11095 2ffaf1e1e101
tuned;
NEWS
     1.1 --- a/NEWS	Sat Feb 10 08:52:41 2001 +0100
     1.2 +++ b/NEWS	Sun Feb 11 13:26:23 2001 +0100
     1.3 @@ -7,12 +7,6 @@
     1.4  
     1.5  *** Overview of INCOMPATIBILITIES ***
     1.6  
     1.7 -* HOL/Algebra: special summation operator SUM no longer exists, it has
     1.8 -been replaced by setsum; infix 'assoc' now has priority 50 (like 'dvd');
     1.9 -
    1.10 -* HOL/Algebra: axiom 'one_not_zero' has been moved from axclass 'ring'
    1.11 -to 'domain', this makes the theory consistent with mathematical literature;
    1.12 - 
    1.13  * HOL: inductive package no longer splits induction rule aggressively,
    1.14  but only as far as specified by the introductions given; the old
    1.15  format may recovered via ML function complete_split_rule or attribute
    1.16 @@ -134,9 +128,15 @@
    1.17  modelling and verification task performed in Isabelle/HOL +
    1.18  Isabelle/Isar + Isabelle document preparation (by Markus Wenzel).
    1.19  
    1.20 +* HOL/Algebra: special summation operator SUM no longer exists, it has
    1.21 +been replaced by setsum; infix 'assoc' now has priority 50 (like
    1.22 +'dvd'); axiom 'one_not_zero' has been moved from axclass 'ring' to
    1.23 +'domain', this makes the theory consistent with mathematical
    1.24 +literature;
    1.25 +
    1.26  * HOL basics: added overloaded operations "inverse" and "divide"
    1.27  (infix "/"), syntax for generic "abs" operation, generic summation
    1.28 -operator;
    1.29 +operator \<Sum>;
    1.30  
    1.31  * HOL/typedef: simplified package, provide more useful rules (see also
    1.32  HOL/subset.thy);
    1.33 @@ -154,7 +154,7 @@
    1.34  * HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals
    1.35  and Fleuriot's mechanization of analysis;
    1.36  
    1.37 -* HOL-Real, HOL-Hyperreals: improved arithmetic simplification;
    1.38 +* HOL/Real, HOL/Hyperreal: improved arithmetic simplification;
    1.39  
    1.40  
    1.41  *** CTT ***