[isabelle] Automatic derivation of a total order on datatypes


is it possible to automa(t/g)ically instantiate a datatype as linorder,
if it is enough that there exists any order (e.g. the order of the
constructors in the definition with the restriction that all arguments
are of class linorder too)?

Use-case: Insert the datatype into a structure that needs an order on
its members. And if one does not care about the specific order, manually
defining it is quite cumbersome (especially for a large number of

Any hints on (semi-)automatic tools/tricks are highly appreciated :)

- René
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.