NEWS
 changeset 16891 20bd6e8c9a4f parent 16888 7cb4bcfa058e child 16908 d374530bfaaa
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.5  * Classical reasoning: the meson method now accepts theorems as arguments.
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.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.27 +* Theory Parity: added rules for simplifying exponents.
1.28 +
1.30  *** HOL-Complex ***
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.57  *** HOLCF ***