src/ZF/Univ.thy

--- a/src/ZF/Univ.thy	Tue Aug 27 11:07:54 2002 +0200
+++ b/src/ZF/Univ.thy	Tue Aug 27 11:09:33 2002 +0200
@@ -192,8 +192,6 @@
 apply (blast intro: ltI Limit_is_Ord)
 done
 
-lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
-
 lemma singleton_in_VLimit:
     "[| a \<in> Vfrom(A,i);  Limit(i) |] ==> {a} \<in> Vfrom(A,i)"
 apply (erule Limit_VfromE, assumption)