* 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