* 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.
Clemens
