diff -r 29ba33d58637 -r 515021e98684 src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Thu Jan 25 09:32:35 2007 +0100
+++ b/src/HOL/Library/Product_ord.thy	Thu Jan 25 09:32:36 2007 +0100
@@ -10,11 +10,16 @@
 begin
 
 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_le_def: "(x \<le> y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x \<le> snd y)"
+  prod_less_def: "(x < y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x < snd y)" ..
 
 lemmas prod_ord_defs = prod_less_def prod_le_def
 
+lemma [code func]:
+  "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
+  "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
+  unfolding prod_ord_defs by simp_all
+
 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"