# HG changeset patch
# User ballarin
# Date 1190133993 -7200
# Node ID e758837c0d184d1112bcf71cab7371c409e6368c
# Parent  c63f98b80bdda922c7990a74ec651daf5e2a07a9
Transitivity reasoner set up for locales.

diff -r c63f98b80bdd -r e758837c0d18 NEWS
--- 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.