diff -r 84a21cf15923 -r 475b321982f7 src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Wed Nov 22 10:20:17 2006 +0100
+++ b/src/HOL/Library/Product_ord.thy	Wed Nov 22 10:20:18 2006 +0100
@@ -9,15 +9,17 @@
 imports Main
 begin
 
-instance "*" :: (ord, ord) ord ..
-
-defs (overloaded)
+instance "*" :: (ord, ord) ord
   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)"
-
+  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
 
+lemma [code]:
+  "(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
+  "(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
+  unfolding prod_ord_defs by simp_all
+
 instance * :: (order, order) order
   by default (auto simp: prod_ord_defs intro: order_less_trans)