--- a/src/HOL/Library/Product_ord.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/Product_ord.thy Sat May 27 17:42:02 2006 +0200
@@ -9,20 +9,19 @@
imports Main
begin
-instance "*" :: (ord,ord) ord ..
+instance "*" :: (ord, ord) ord ..
defs (overloaded)
- prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)"
+ prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)"
prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)"
lemmas prod_ord_defs = prod_less_def prod_le_def
-instance "*" :: (order,order) order
- apply (intro_classes, unfold prod_ord_defs)
- by (auto intro: order_less_trans)
+instance * :: (order, order) order
+ by default (auto simp: prod_ord_defs intro: order_less_trans)
-instance "*":: (linorder,linorder)linorder
- by (intro_classes, unfold prod_le_def, auto)
+instance * :: (linorder, linorder) linorder
+ by default (auto simp: prod_le_def)
-end
\ No newline at end of file
+end