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

NEWS

changeset 14398 | c5c47703f763 |

parent 14389 | 57c2d90936ba |

child 14399 | dc677b35e54f |

1.1 --- a/NEWS Thu Feb 19 10:41:32 2004 +0100 1.2 +++ b/NEWS Thu Feb 19 15:57:34 2004 +0100 1.3 @@ -6,6 +6,9 @@ 1.4 1.5 *** General *** 1.6 1.7 +* Provers/order.ML: new efficient reasoner for partial and linear orders. 1.8 + Replaces linorder.ML. 1.9 + 1.10 * Pure: Greek letters (except small lambda, \<lambda>), as well as gothic 1.11 (\<aa>...\<zz>\<AA>...\<ZZ>), caligraphic (\<A>...\<Z>), and euler 1.12 (\<a>...\<z>), are now considered normal letters, and can therefore 1.13 @@ -77,6 +80,16 @@ 1.14 1.15 *** HOL *** 1.16 1.17 +* Simplifier: 1.18 + - Much improved handling of linear and partial orders. 1.19 + Reasoners for linear and partial orders are set up for type classes 1.20 + "linorder" and "order" respectively, and are added to the default simpset 1.21 + as solvers. This means that the simplifier can build transitivity chains 1.22 + to solve goals from the assumptions. 1.23 + - INCOMPATIBILITY: old proofs break occasionally. Typically, applications 1.24 + of blast or auto after simplification become unnecessary because the goal 1.25 + is solved by simplification already. 1.26 + 1.27 * Numerics: new theory Ring_and_Field contains over 250 basic numerical laws, 1.28 all proved in axiomatic type classes for semirings, rings and fields. 1.29