[isabelle-dev] NEWS: transitivity reasoner

Clemens Ballarin ballarin at in.tum.de
Wed Sep 19 11:43:42 CEST 2007

* The transitivity reasoner for partial and linear orders is set up for
locales `order' and `linorder' generated by the new class package.   
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  


More information about the isabelle-dev mailing list