--- a/src/ZF/Arith.thy Tue May 28 11:06:55 2002 +0200
+++ b/src/ZF/Arith.thy Tue May 28 11:07:36 2002 +0200
@@ -497,7 +497,6 @@
val div_def = thm "div_def";
val mod_def = thm "mod_def";
-val zero_lt_lemma = thm "zero_lt_lemma";
val zero_lt_natE = thm "zero_lt_natE";
val pred_succ_eq = thm "pred_succ_eq";
val natify_succ = thm "natify_succ";
--- a/src/ZF/Epsilon.thy Tue May 28 11:06:55 2002 +0200
+++ b/src/ZF/Epsilon.thy Tue May 28 11:07:36 2002 +0200
@@ -357,8 +357,7 @@
a: C(0);
!!m z. [| m: nat; z: C(m) |] ==> b(m,z): C(succ(m)) |]
==> rec(n,a,b) : C(n)"
-apply (erule nat_induct, auto)
-done
+by (erule nat_induct, auto)
ML
{*
@@ -371,7 +370,6 @@
val arg_into_eclose_sing = thm "arg_into_eclose_sing";
val eclose_induct = thm "eclose_induct";
val eps_induct = thm "eps_induct";
-val eclose_least_lemma = thm "eclose_least_lemma";
val eclose_least = thm "eclose_least";
val eclose_induct_down = thm "eclose_induct_down";
val Transset_eclose_eq_arg = thm "Transset_eclose_eq_arg";
@@ -408,7 +406,6 @@
val transrec2_0 = thm "transrec2_0";
val transrec2_succ = thm "transrec2_succ";
val transrec2_Limit = thm "transrec2_Limit";
-val recursor_lemma = thm "recursor_lemma";
val recursor_0 = thm "recursor_0";
val recursor_succ = thm "recursor_succ";
val rec_0 = thm "rec_0";
--- a/src/ZF/Nat.thy Tue May 28 11:06:55 2002 +0200
+++ b/src/ZF/Nat.thy Tue May 28 11:07:36 2002 +0200
@@ -299,10 +299,8 @@
val lt_nat_in_nat = thm "lt_nat_in_nat";
val le_in_nat = thm "le_in_nat";
val complete_induct = thm "complete_induct";
-val nat_induct_from_lemma = thm "nat_induct_from_lemma";
val nat_induct_from = thm "nat_induct_from";
val diff_induct = thm "diff_induct";
-val succ_lt_induct_lemma = thm "succ_lt_induct_lemma";
val succ_lt_induct = thm "succ_lt_induct";
val nat_case_0 = thm "nat_case_0";
val nat_case_succ = thm "nat_case_succ";
--- a/src/ZF/Order.thy Tue May 28 11:06:55 2002 +0200
+++ b/src/ZF/Order.thy Tue May 28 11:07:36 2002 +0200
@@ -685,13 +685,11 @@
val linear_ord_iso = thm "linear_ord_iso";
val wf_on_ord_iso = thm "wf_on_ord_iso";
val well_ord_ord_iso = thm "well_ord_ord_iso";
-val well_ord_iso_subset_lemma = thm "well_ord_iso_subset_lemma";
val well_ord_iso_predE = thm "well_ord_iso_predE";
val well_ord_iso_pred_eq = thm "well_ord_iso_pred_eq";
val ord_iso_image_pred = thm "ord_iso_image_pred";
val ord_iso_restrict_pred = thm "ord_iso_restrict_pred";
val well_ord_iso_preserving = thm "well_ord_iso_preserving";
-val well_ord_iso_unique_lemma = thm "well_ord_iso_unique_lemma";
val well_ord_iso_unique = thm "well_ord_iso_unique";
val ord_iso_map_subset = thm "ord_iso_map_subset";
val domain_ord_iso_map = thm "domain_ord_iso_map";
--- a/src/ZF/OrderType.thy Tue May 28 11:06:55 2002 +0200
+++ b/src/ZF/OrderType.thy Tue May 28 11:07:36 2002 +0200
@@ -922,7 +922,6 @@
val well_ord_Memrel = thm "well_ord_Memrel";
val lt_pred_Memrel = thm "lt_pred_Memrel";
val pred_Memrel = thm "pred_Memrel";
-val Ord_iso_implies_eq_lemma = thm "Ord_iso_implies_eq_lemma";
val Ord_iso_implies_eq = thm "Ord_iso_implies_eq";
val ordermap_type = thm "ordermap_type";
val ordermap_eq_image = thm "ordermap_eq_image";
@@ -996,7 +995,6 @@
val Ord_omult = thm "Ord_omult";
val pred_Pair_eq = thm "pred_Pair_eq";
val ordertype_pred_Pair_eq = thm "ordertype_pred_Pair_eq";
-val ordertype_pred_Pair_lemma = thm "ordertype_pred_Pair_lemma";
val lt_omult = thm "lt_omult";
val omult_oadd_lt = thm "omult_oadd_lt";
val omult_unfold = thm "omult_unfold";
--- a/src/ZF/Perm.thy Tue May 28 11:06:55 2002 +0200
+++ b/src/ZF/Perm.thy Tue May 28 11:07:36 2002 +0200
@@ -568,10 +568,8 @@
val id_bij = thm "id_bij";
val subset_iff_id = thm "subset_iff_id";
val inj_converse_fun = thm "inj_converse_fun";
-val left_inverse_lemma = thm "left_inverse_lemma";
val left_inverse = thm "left_inverse";
val left_inverse_bij = thm "left_inverse_bij";
-val right_inverse_lemma = thm "right_inverse_lemma";
val right_inverse = thm "right_inverse";
val right_inverse_bij = thm "right_inverse_bij";
val inj_converse_inj = thm "inj_converse_inj";
--- 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";