Transitivity reasoner set up for locales.

--- a/NEWS	Tue Sep 18 18:06:47 2007 +0200
+++ b/NEWS	Tue Sep 18 18:46:33 2007 +0200
@@ -517,6 +517,16 @@
 
 *** HOL ***
 
+* The transitivity reasoner for partial and linear orders is set up for
+locales `order' and `linorder' generated by the new class package.  Previously
+the reasoner was only set up for axiomatic type classes.  Instances of the
+reasoner are available in all contexts importing or interpreting these locales.
+The following functionality is provided:
+  - method `order' to invoke the reasoner manually.
+  - diagnostic command `print_orders' shows which instances of the reasoner are
+    available in the current context.
+As previously, the reasoner is integrated with the simplifier as a solver. 
+
 * Formulation of theorem "dense" changed slightly due to integration with new
 class dense_linear_order.