src/ZF/pair.thy
changeset 45602 2a858377c3d2
parent 42795 66fcc9882784
child 45620 f2a587696afb
     1.1 --- a/src/ZF/pair.thy	Sun Nov 20 17:57:09 2011 +0100
     1.2 +++ b/src/ZF/pair.thy	Sun Nov 20 20:15:02 2011 +0100
     1.3 @@ -43,17 +43,17 @@
     1.4  lemma Pair_iff [simp]: "<a,b> = <c,d> <-> a=c & b=d"
     1.5  by (simp add: Pair_def doubleton_eq_iff, blast)
     1.6  
     1.7 -lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, standard, elim!]
     1.8 +lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, elim!]
     1.9  
    1.10 -lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1, standard]
    1.11 -lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2, standard]
    1.12 +lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1]
    1.13 +lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2]
    1.14  
    1.15  lemma Pair_not_0: "<a,b> ~= 0"
    1.16  apply (unfold Pair_def)
    1.17  apply (blast elim: equalityE)
    1.18  done
    1.19  
    1.20 -lemmas Pair_neq_0 = Pair_not_0 [THEN notE, standard, elim!]
    1.21 +lemmas Pair_neq_0 = Pair_not_0 [THEN notE, elim!]
    1.22  
    1.23  declare sym [THEN Pair_neq_0, elim!]
    1.24  
    1.25 @@ -82,8 +82,8 @@
    1.26  lemma SigmaI [TC,intro!]: "[| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)"
    1.27  by simp
    1.28  
    1.29 -lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1, standard]
    1.30 -lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2, standard]
    1.31 +lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1]
    1.32 +lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2]
    1.33  
    1.34  (*The general elimination rule*)
    1.35  lemma SigmaE [elim!]: