author wenzelm Tue, 19 Jul 2005 17:54:32 +0200 changeset 16891 20bd6e8c9a4f parent 16890 c4e5afaba440 child 16892 23887fee6071
tuned;
 NEWS file | annotate | diff | comparison | revisions
```--- 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 ***```