# HG changeset patch
# User haftmann
# Date 1223388444 -7200
# Node ID 095fe24b48fdea21ca8ff403349d7da669c179da
# Parent  0329689a112722967f84d9fa69c50173317c6a41
code generator more liberal with respect to sort constraints of instance parameters

diff -r 0329689a1127 -r 095fe24b48fd src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Tue Oct 07 16:07:23 2008 +0200
+++ b/src/HOL/Library/Product_ord.thy	Tue Oct 07 16:07:24 2008 +0200
@@ -22,11 +22,6 @@
 
 end
 
-lemma [code, code func del]:
-  "(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_le_def prod_less_def by simp_all
-
 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"