1.1 --- a/NEWS	Tue Jul 19 17:28:37 2005 +0200
     1.2 +++ b/NEWS	Tue Jul 19 17:54:32 2005 +0200
     1.3 @@ -351,13 +351,12 @@
     1.4  
     1.5  * Classical reasoning: the meson method now accepts theorems as arguments.
     1.6  
     1.7 -* Introduced various additions and improvements in OrderedGroup.thy and 
     1.8 -Ring_and_Field.thy, to faciliate calculations involving equalities 
     1.9 -and inequalities.
    1.10 -
    1.11 -* Added rules for simplifying exponents to Parity.thy
    1.12 -
    1.13 -Below are some theorems that have been eliminated or modified in this release:
    1.14 +* Theory OrderedGroup and Ring_and_Field: various additions and
    1.15 +improvements to faciliate calculations involving equalities and
    1.16 +inequalities.
    1.17 +
    1.18 +The following theorems have been eliminated or modified
    1.19 +(INCOMPATIBILITY):
    1.20  
    1.21    abs_eq             now named abs_of_nonneg
    1.22    abs_of_ge_0        now named abs_of_nonneg 
    1.23 @@ -371,20 +370,23 @@
    1.24    mult_neg           now named mult_neg_neg
    1.25    mult_neg_le        now named mult_nonpos_nonpos
    1.26  
    1.27 +* Theory Parity: added rules for simplifying exponents.
    1.28 +
    1.29  
    1.30  *** HOL-Complex ***
    1.31  
    1.32 -* Introduced better support for embedding natural numbers and integers
    1.33 -in the reals, in RealDef.thy.
    1.34 -
    1.35 -* Expanded support for floor and ceiling functions, in RComplete.thy.
    1.36 -
    1.37 -Below are some theorems that have been eliminated or modified in this release:
    1.38 -
    1.39 -  real_of_int_add    reversed direction of equality (use "THEN sym")
    1.40 -  real_of_int_minus  reversed direction of equality (use "THEN sym")
    1.41 -  real_of_int_diff   reversed direction of equality (use "THEN sym")
    1.42 -  real_of_int_mult   reversed direction of equality (use "THEN sym")
    1.43 +* Theory RealDef: better support for embedding natural numbers and
    1.44 +integers in the reals.
    1.45 +
    1.46 +The following theorems have been eliminated or modified
    1.47 +(INCOMPATIBILITY):
    1.48 +
    1.49 +  real_of_int_add    reversed direction of equality (use [symmetric])
    1.50 +  real_of_int_minus  reversed direction of equality (use [symmetric])
    1.51 +  real_of_int_diff   reversed direction of equality (use [symmetric])
    1.52 +  real_of_int_mult   reversed direction of equality (use [symmetric])
    1.53 +
    1.54 +* Theory RComplete: expanded support for floor and ceiling functions.
    1.55  
    1.56  
    1.57  *** HOLCF ***