src/ZF/Epsilon.thy
changeset 58860 fee7cfa69c50
parent 46953 2b6e55924af3
child 58871 c399ae4b836f
     1.1 --- a/src/ZF/Epsilon.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/ZF/Epsilon.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -117,14 +117,14 @@
     1.4  done
     1.5  
     1.6  text{*A transitive set either is empty or contains the empty set.*}
     1.7 -lemma Transset_0_lemma [rule_format]: "Transset(A) ==> x\<in>A \<longrightarrow> 0\<in>A";
     1.8 +lemma Transset_0_lemma [rule_format]: "Transset(A) ==> x\<in>A \<longrightarrow> 0\<in>A"
     1.9  apply (simp add: Transset_def)
    1.10  apply (rule_tac a=x in eps_induct, clarify)
    1.11  apply (drule bspec, assumption)
    1.12  apply (case_tac "x=0", auto)
    1.13  done
    1.14  
    1.15 -lemma Transset_0_disj: "Transset(A) ==> A=0 | 0\<in>A";
    1.16 +lemma Transset_0_disj: "Transset(A) ==> A=0 | 0\<in>A"
    1.17  by (blast dest: Transset_0_lemma)
    1.18  
    1.19