summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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.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 +* 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.20 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.26 1.27 +* Theory Parity: added rules for simplifying exponents. 1.28 + 1.29 1.30 *** HOL-Complex *** 1.31 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.55 1.56 1.57 *** HOLCF ***