src/ZF/Sum.thy
changeset 45602 2a858377c3d2
parent 41777 1f7cbe39d425
child 46820 c656222c4dc1
     1.1 --- a/src/ZF/Sum.thy	Sun Nov 20 17:57:09 2011 +0100
     1.2 +++ b/src/ZF/Sum.thy	Sun Nov 20 20:15:02 2011 +0100
     1.3 @@ -94,8 +94,8 @@
     1.4  
     1.5  (*Injection and freeness rules*)
     1.6  
     1.7 -lemmas Inl_inject = Inl_iff [THEN iffD1, standard]
     1.8 -lemmas Inr_inject = Inr_iff [THEN iffD1, standard]
     1.9 +lemmas Inl_inject = Inl_iff [THEN iffD1]
    1.10 +lemmas Inr_inject = Inr_iff [THEN iffD1]
    1.11  lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE, elim!]
    1.12  lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE, elim!]
    1.13  
    1.14 @@ -168,7 +168,7 @@
    1.15  by blast
    1.16  
    1.17  lemmas Part_CollectE =
    1.18 -     Part_Collect [THEN equalityD1, THEN subsetD, THEN CollectE, standard]
    1.19 +     Part_Collect [THEN equalityD1, THEN subsetD, THEN CollectE]
    1.20  
    1.21  lemma Part_Inl: "Part(A+B,Inl) = {Inl(x). x: A}"
    1.22  by blast