diff -r b3b15305a1c9 -r c5c47703f763 NEWS
--- 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.