[isabelle-dev] NEWS: transitivity reasoner

[Clemens Ballarin]

* 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