src/HOL/Sum_Type.thy
changeset 21454 a1937c51ed88
parent 21046 fe1db2f991a7
child 22424 8a5412121687
     1.1 --- a/src/HOL/Sum_Type.thy	Wed Nov 22 10:20:11 2006 +0100
     1.2 +++ b/src/HOL/Sum_Type.thy	Wed Nov 22 10:20:12 2006 +0100
     1.3 @@ -197,20 +197,20 @@
     1.4  instance "+" :: (eq, eq) eq ..
     1.5  
     1.6  lemma [code func]:
     1.7 -  "Code_Generator.eq (Inl x) (Inl y) = Code_Generator.eq x y"
     1.8 -  unfolding eq_def Inl_eq ..
     1.9 +  "(Inl x \<Colon> 'a\<Colon>eq + 'b\<Colon>eq) = Inl y \<longleftrightarrow> x = y"
    1.10 +  unfolding Inl_eq ..
    1.11  
    1.12  lemma [code func]:
    1.13 -  "Code_Generator.eq (Inr x) (Inr y) = Code_Generator.eq x y"
    1.14 -  unfolding eq_def Inr_eq ..
    1.15 +  "(Inr x \<Colon> 'a\<Colon>eq + 'b\<Colon>eq) = Inr y \<longleftrightarrow> x = y"
    1.16 +  unfolding Inr_eq ..
    1.17  
    1.18  lemma [code func]:
    1.19 -  "Code_Generator.eq (Inl x) (Inr y) = False"
    1.20 -  unfolding eq_def using Inl_not_Inr by auto
    1.21 +  "Inl (x\<Colon>'a\<Colon>eq) = Inr (y\<Colon>'b\<Colon>eq) \<longleftrightarrow> False"
    1.22 +  using Inl_not_Inr by auto
    1.23  
    1.24  lemma [code func]:
    1.25 -  "Code_Generator.eq (Inr x) (Inl y) = False"
    1.26 -  unfolding eq_def using Inr_not_Inl by auto
    1.27 +  "Inr (x\<Colon>'b\<Colon>eq) = Inl (y\<Colon>'a\<Colon>eq) \<longleftrightarrow> False"
    1.28 +  using Inr_not_Inl by auto
    1.29  
    1.30  ML
    1.31  {*