# HG changeset patch # User paulson # Date 1022576856 -7200 # Node ID da61bfa0a391bbc0f58411967cef91c95b6f92b7 # Parent 197e5a88c9dfc57aa82b1081b07b8713a76650c6 deleted some useless ML bindings diff -r 197e5a88c9df -r da61bfa0a391 src/ZF/Arith.thy --- 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"; diff -r 197e5a88c9df -r da61bfa0a391 src/ZF/Epsilon.thy --- 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"; diff -r 197e5a88c9df -r da61bfa0a391 src/ZF/Nat.thy --- 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"; diff -r 197e5a88c9df -r da61bfa0a391 src/ZF/Order.thy --- 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"; diff -r 197e5a88c9df -r da61bfa0a391 src/ZF/OrderType.thy --- 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"; diff -r 197e5a88c9df -r da61bfa0a391 src/ZF/Perm.thy --- 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"; diff -r 197e5a88c9df -r da61bfa0a391 src/ZF/Univ.thy --- 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";