[isabelle] type classes

It seems to me that one ought to be able to prove

Goal "OFCLASS ('b :: ord, order_class) ==>
 ((x :: 'b) <= y) = (x < y | x = y)" ;

(where the consequent is just a theorem of the order class, in this case

      (["Orderings.order_le_less"], "(?x <= ?y) = (?x < ?y | ?x = ?y)"),

How can one use the theorem order_le_less to prove this goal?


Jeremy Dawson

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