[isabelle-dev] NEWS: transitivity reasoner
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
reasoner are available in all contexts importing or interpreting
The following functionality is provided:
- method `order' to invoke the reasoner manually.
- diagnostic command `print_orders' shows which instances of the
available in the current context.
As previously, the reasoner is integrated with the simplifier as a
More information about the isabelle-dev