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