summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

NEWS

changeset 17016 | 73c74cb1d744 |

parent 16997 | 7dfc99f62dd9 |

child 17047 | e2e2d75bb37b |

--- a/NEWS Wed Aug 03 14:48:56 2005 +0200 +++ b/NEWS Wed Aug 03 14:49:04 2005 +0200 @@ -261,7 +261,8 @@ * "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x". Similarly for all quantifiers: "ALL x > y" etc. The x-symbol for >= -is \<ge>. +is \<ge>. New transitivity rules have been added to HOL/Orderings.thy to +support corresponding Isar calculations. * "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\<in>" instead of ":". @@ -384,10 +385,11 @@ 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]) + exp_ge_add_one_self now requires no hypotheses + 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.