src/ZF/Epsilon.thy
changeset 14153 76a6ba67bd15
parent 13784 b9f6154427a4
child 15481 fc075ae929e4
     1.1 --- a/src/ZF/Epsilon.thy	Tue Aug 19 13:53:58 2003 +0200
     1.2 +++ b/src/ZF/Epsilon.thy	Tue Aug 19 13:54:20 2003 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4  apply (simp add: Transset_def) 
     1.5  apply (rule_tac a=x in eps_induct, clarify) 
     1.6  apply (drule bspec, assumption) 
     1.7 -apply (rule_tac P = "x=0" in case_split_thm, auto)
     1.8 +apply (case_tac "x=0", auto)
     1.9  done
    1.10  
    1.11  lemma Transset_0_disj: "Transset(A) ==> A=0 | 0\<in>A";