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

NEWS

changeset 14398 | c5c47703f763 |

parent 14389 | 57c2d90936ba |

child 14399 | dc677b35e54f |

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