diff -r c4e5afaba440 -r 20bd6e8c9a4f NEWS
--- a/NEWS	Tue Jul 19 17:28:37 2005 +0200
+++ b/NEWS	Tue Jul 19 17:54:32 2005 +0200
@@ -351,13 +351,12 @@
 
 * Classical reasoning: the meson method now accepts theorems as arguments.
 
-* Introduced various additions and improvements in OrderedGroup.thy and 
-Ring_and_Field.thy, to faciliate calculations involving equalities 
-and inequalities.
-
-* Added rules for simplifying exponents to Parity.thy
-
-Below are some theorems that have been eliminated or modified in this release:
+* Theory OrderedGroup and Ring_and_Field: various additions and
+improvements to faciliate calculations involving equalities and
+inequalities.
+
+The following theorems have been eliminated or modified
+(INCOMPATIBILITY):
 
   abs_eq             now named abs_of_nonneg
   abs_of_ge_0        now named abs_of_nonneg 
@@ -371,20 +370,23 @@
   mult_neg           now named mult_neg_neg
   mult_neg_le        now named mult_nonpos_nonpos
 
+* Theory Parity: added rules for simplifying exponents.
+
 
 *** HOL-Complex ***
 
-* Introduced better support for embedding natural numbers and integers
-in the reals, in RealDef.thy.
-
-* Expanded support for floor and ceiling functions, in RComplete.thy.
-
-Below are some theorems that have been eliminated or modified in this release:
-
-  real_of_int_add    reversed direction of equality (use "THEN sym")
-  real_of_int_minus  reversed direction of equality (use "THEN sym")
-  real_of_int_diff   reversed direction of equality (use "THEN sym")
-  real_of_int_mult   reversed direction of equality (use "THEN sym")
+* Theory RealDef: better support for embedding natural numbers and
+integers in the reals.
+
+The following theorems have been eliminated or modified
+(INCOMPATIBILITY):
+
+  real_of_int_add    reversed direction of equality (use [symmetric])
+  real_of_int_minus  reversed direction of equality (use [symmetric])
+  real_of_int_diff   reversed direction of equality (use [symmetric])
+  real_of_int_mult   reversed direction of equality (use [symmetric])
+
+* Theory RComplete: expanded support for floor and ceiling functions.
 
 
 *** HOLCF ***