diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Library/Product_ord.thy
--- 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