code generator more liberal with respect to sort constraints of instance parameters
authorhaftmann
Tue Oct 07 16:07:24 2008 +0200 (2008-10-07)
changeset 28519095fe24b48fd
parent 28518 0329689a1127
child 28520 376b9c083b04
code generator more liberal with respect to sort constraints of instance parameters
src/HOL/Library/Product_ord.thy
     1.1 --- a/src/HOL/Library/Product_ord.thy	Tue Oct 07 16:07:23 2008 +0200
     1.2 +++ b/src/HOL/Library/Product_ord.thy	Tue Oct 07 16:07:24 2008 +0200
     1.3 @@ -22,11 +22,6 @@
     1.4  
     1.5  end
     1.6  
     1.7 -lemma [code, code func del]:
     1.8 -  "(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
     1.9 -  "(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
    1.10 -  unfolding prod_le_def prod_less_def by simp_all
    1.11 -
    1.12  lemma [code func]:
    1.13    "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
    1.14    "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"