--- a/src/ZF/Univ.thy Tue May 28 11:06:55 2002 +0200
+++ b/src/ZF/Univ.thy Tue May 28 11:07:36 2002 +0200
@@ -790,7 +790,6 @@
val Pair_in_Vfrom = thm "Pair_in_Vfrom";
val succ_in_Vfrom = thm "succ_in_Vfrom";
val Vfrom_0 = thm "Vfrom_0";
-val Vfrom_succ_lemma = thm "Vfrom_succ_lemma";
val Vfrom_succ = thm "Vfrom_succ";
val Vfrom_Union = thm "Vfrom_Union";
val Limit_Vfrom_eq = thm "Limit_Vfrom_eq";
@@ -831,7 +830,6 @@
val Vset_succ = thm "Vset_succ";
val Transset_Vset = thm "Transset_Vset";
val VsetD = thm "VsetD";
-val VsetI_lemma = thm "VsetI_lemma";
val VsetI = thm "VsetI";
val Vset_Ord_rank_iff = thm "Vset_Ord_rank_iff";
val Vset_rank_iff = thm "Vset_rank_iff";
@@ -868,7 +866,6 @@
val Inr_in_univ = thm "Inr_in_univ";
val sum_univ = thm "sum_univ";
val sum_subset_univ = thm "sum_subset_univ";
-val Fin_Vfrom_lemma = thm "Fin_Vfrom_lemma";
val Fin_VLimit = thm "Fin_VLimit";
val Fin_subset_VLimit = thm "Fin_subset_VLimit";
val Fin_univ = thm "Fin_univ";