src/ZF/Sum.thy
changeset 13823 d49ffd9f9662
parent 13356 c9cfe1638bf2
child 16417 9bc16273c2d4
     1.1 --- a/src/ZF/Sum.thy	Tue Feb 18 19:13:47 2003 +0100
     1.2 +++ b/src/ZF/Sum.thy	Wed Feb 19 10:53:27 2003 +0100
     1.3 @@ -90,10 +90,10 @@
     1.4  lemma Inr_iff [iff]: "Inr(a)=Inr(b) <-> a=b"
     1.5  by (simp add: sum_defs)
     1.6  
     1.7 -lemma Inl_Inr_iff [iff]: "Inl(a)=Inr(b) <-> False"
     1.8 +lemma Inl_Inr_iff [simp]: "Inl(a)=Inr(b) <-> False"
     1.9  by (simp add: sum_defs)
    1.10  
    1.11 -lemma Inr_Inl_iff [iff]: "Inr(b)=Inl(a) <-> False"
    1.12 +lemma Inr_Inl_iff [simp]: "Inr(b)=Inl(a) <-> False"
    1.13  by (simp add: sum_defs)
    1.14  
    1.15  lemma sum_empty [simp]: "0+0 = 0"
    1.16 @@ -103,8 +103,8 @@
    1.17  
    1.18  lemmas Inl_inject = Inl_iff [THEN iffD1, standard]
    1.19  lemmas Inr_inject = Inr_iff [THEN iffD1, standard]
    1.20 -lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE]
    1.21 -lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE]
    1.22 +lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE, elim!]
    1.23 +lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE, elim!]
    1.24  
    1.25  
    1.26  lemma InlD: "Inl(a): A+B ==> a: A"