src/HOL/Sum_Type.thy
changeset 29025 8c8859c0d734
parent 28524 644b62cf678f
child 29183 f1648e009dc1
     1.1 --- a/src/HOL/Sum_Type.thy	Tue Dec 09 12:53:25 2008 -0800
     1.2 +++ b/src/HOL/Sum_Type.thy	Tue Dec 09 15:31:38 2008 -0800
     1.3 @@ -93,16 +93,17 @@
     1.4  lemma Inr_Rep_inject: "Inr_Rep(b) = Inr_Rep(d) ==> b=d"
     1.5  by (auto simp add: Inr_Rep_def expand_fun_eq)
     1.6  
     1.7 -lemma inj_Inl: "inj(Inl)"
     1.8 +lemma inj_Inl [simp]: "inj_on Inl A"
     1.9  apply (simp add: Inl_def)
    1.10  apply (rule inj_onI)
    1.11  apply (erule inj_on_Abs_Sum [THEN inj_onD, THEN Inl_Rep_inject])
    1.12  apply (rule Inl_RepI)
    1.13  apply (rule Inl_RepI)
    1.14  done
    1.15 +
    1.16  lemmas Inl_inject = inj_Inl [THEN injD, standard]
    1.17  
    1.18 -lemma inj_Inr: "inj(Inr)"
    1.19 +lemma inj_Inr [simp]: "inj_on Inr A"
    1.20  apply (simp add: Inr_def)
    1.21  apply (rule inj_onI)
    1.22  apply (erule inj_on_Abs_Sum [THEN inj_onD, THEN Inr_Rep_inject])