summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 19 Jul 2005 17:54:32 +0200 | |

changeset 16891 | 20bd6e8c9a4f |

parent 16890 | c4e5afaba440 |

child 16892 | 23887fee6071 |

tuned;

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