src/HOL/Sum_Type.thy
changeset 25534 d0b74fdd6067
parent 22838 466599ecf610
child 27104 791607529f6d
     1.1 --- a/src/HOL/Sum_Type.thy	Wed Dec 05 14:15:39 2007 +0100
     1.2 +++ b/src/HOL/Sum_Type.thy	Wed Dec 05 14:15:45 2007 +0100
     1.3 @@ -215,26 +215,6 @@
     1.4  by blast
     1.5  
     1.6  
     1.7 -subsection {* Code generator setup *}
     1.8 -
     1.9 -instance "+" :: (eq, eq) eq ..
    1.10 -
    1.11 -lemma [code func]:
    1.12 -  "(Inl x \<Colon> 'a\<Colon>eq + 'b\<Colon>eq) = Inl y \<longleftrightarrow> x = y"
    1.13 -  unfolding Inl_eq ..
    1.14 -
    1.15 -lemma [code func]:
    1.16 -  "(Inr x \<Colon> 'a\<Colon>eq + 'b\<Colon>eq) = Inr y \<longleftrightarrow> x = y"
    1.17 -  unfolding Inr_eq ..
    1.18 -
    1.19 -lemma [code func]:
    1.20 -  "Inl (x\<Colon>'a\<Colon>eq) = Inr (y\<Colon>'b\<Colon>eq) \<longleftrightarrow> False"
    1.21 -  using Inl_not_Inr by auto
    1.22 -
    1.23 -lemma [code func]:
    1.24 -  "Inr (x\<Colon>'b\<Colon>eq) = Inl (y\<Colon>'a\<Colon>eq) \<longleftrightarrow> False"
    1.25 -  using Inr_not_Inl by auto
    1.26 -
    1.27  ML
    1.28  {*
    1.29  val Inl_RepI = thm "Inl_RepI";