--- 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 ***