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

author | avigad |

Wed, 03 Aug 2005 14:49:04 +0200 | |

changeset 17016 | 73c74cb1d744 |

parent 17015 | 50e1d2be7e67 |

child 17017 | fa8e32209734 |

mentioned change to exp_ge_add_one_self, new transitivity rules

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