1.1 --- a/NEWS Tue Jul 19 17:21:59 2005 +0200
1.2 +++ b/NEWS Tue Jul 19 17:24:09 2005 +0200
1.3 @@ -351,6 +351,41 @@
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 +
1.15 + abs_eq now named abs_of_nonneg
1.16 + abs_of_ge_0 now named abs_of_nonneg
1.17 + abs_minus_eq now named abs_of_nonpos
1.18 + imp_abs_id now named abs_of_nonneg
1.19 + imp_abs_neg_id now named abs_of_nonpos
1.20 + mult_pos now named mult_pos_pos
1.21 + mult_pos_le now named mult_nonneg_nonneg
1.22 + mult_pos_neg_le now named mult_nonneg_nonpos
1.23 + mult_pos_neg2_le now named mult_nonneg_nonpos2
1.24 + mult_neg now named mult_neg_neg
1.25 + mult_neg_le now named mult_nonpos_nonpos
1.26 +
1.27 +
1.28 +*** HOL-Complex ***
1.29 +
1.30 +* Introduced better support for embedding natural numbers and integers
1.31 +in the reals, in RealDef.thy.
1.32 +
1.33 +* Expanded support for floor and ceiling functions, in RComplete.thy.
1.34 +
1.35 +Below are some theorems that have been eliminated or modified in this release:
1.36 +
1.37 + real_of_int_add reversed direction of equality (use "THEN sym")
1.38 + real_of_int_minus reversed direction of equality (use "THEN sym")
1.39 + real_of_int_diff reversed direction of equality (use "THEN sym")
1.40 + real_of_int_mult reversed direction of equality (use "THEN sym")
1.41 +
1.42
1.43 *** HOLCF ***
1.44