deleted some useless ML bindings
authorpaulson
Tue May 28 11:07:36 2002 +0200 (2002-05-28)
changeset 13185da61bfa0a391
parent 13184 197e5a88c9df
child 13186 ef8ed6adcb38
deleted some useless ML bindings
src/ZF/Arith.thy
src/ZF/Epsilon.thy
src/ZF/Nat.thy
src/ZF/Order.thy
src/ZF/OrderType.thy
src/ZF/Perm.thy
src/ZF/Univ.thy
     1.1 --- a/src/ZF/Arith.thy	Tue May 28 11:06:55 2002 +0200
     1.2 +++ b/src/ZF/Arith.thy	Tue May 28 11:07:36 2002 +0200
     1.3 @@ -497,7 +497,6 @@
     1.4  val div_def = thm "div_def";
     1.5  val mod_def = thm "mod_def";
     1.6  
     1.7 -val zero_lt_lemma = thm "zero_lt_lemma";
     1.8  val zero_lt_natE = thm "zero_lt_natE";
     1.9  val pred_succ_eq = thm "pred_succ_eq";
    1.10  val natify_succ = thm "natify_succ";
     2.1 --- a/src/ZF/Epsilon.thy	Tue May 28 11:06:55 2002 +0200
     2.2 +++ b/src/ZF/Epsilon.thy	Tue May 28 11:07:36 2002 +0200
     2.3 @@ -357,8 +357,7 @@
     2.4          a: C(0);   
     2.5          !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m)) |]
     2.6       ==> rec(n,a,b) : C(n)"
     2.7 -apply (erule nat_induct, auto)
     2.8 -done
     2.9 +by (erule nat_induct, auto)
    2.10  
    2.11  ML
    2.12  {*
    2.13 @@ -371,7 +370,6 @@
    2.14  val arg_into_eclose_sing = thm "arg_into_eclose_sing";
    2.15  val eclose_induct = thm "eclose_induct";
    2.16  val eps_induct = thm "eps_induct";
    2.17 -val eclose_least_lemma = thm "eclose_least_lemma";
    2.18  val eclose_least = thm "eclose_least";
    2.19  val eclose_induct_down = thm "eclose_induct_down";
    2.20  val Transset_eclose_eq_arg = thm "Transset_eclose_eq_arg";
    2.21 @@ -408,7 +406,6 @@
    2.22  val transrec2_0 = thm "transrec2_0";
    2.23  val transrec2_succ = thm "transrec2_succ";
    2.24  val transrec2_Limit = thm "transrec2_Limit";
    2.25 -val recursor_lemma = thm "recursor_lemma";
    2.26  val recursor_0 = thm "recursor_0";
    2.27  val recursor_succ = thm "recursor_succ";
    2.28  val rec_0 = thm "rec_0";
     3.1 --- a/src/ZF/Nat.thy	Tue May 28 11:06:55 2002 +0200
     3.2 +++ b/src/ZF/Nat.thy	Tue May 28 11:07:36 2002 +0200
     3.3 @@ -299,10 +299,8 @@
     3.4  val lt_nat_in_nat = thm "lt_nat_in_nat";
     3.5  val le_in_nat = thm "le_in_nat";
     3.6  val complete_induct = thm "complete_induct";
     3.7 -val nat_induct_from_lemma = thm "nat_induct_from_lemma";
     3.8  val nat_induct_from = thm "nat_induct_from";
     3.9  val diff_induct = thm "diff_induct";
    3.10 -val succ_lt_induct_lemma = thm "succ_lt_induct_lemma";
    3.11  val succ_lt_induct = thm "succ_lt_induct";
    3.12  val nat_case_0 = thm "nat_case_0";
    3.13  val nat_case_succ = thm "nat_case_succ";
     4.1 --- a/src/ZF/Order.thy	Tue May 28 11:06:55 2002 +0200
     4.2 +++ b/src/ZF/Order.thy	Tue May 28 11:07:36 2002 +0200
     4.3 @@ -685,13 +685,11 @@
     4.4  val linear_ord_iso = thm "linear_ord_iso";
     4.5  val wf_on_ord_iso = thm "wf_on_ord_iso";
     4.6  val well_ord_ord_iso = thm "well_ord_ord_iso";
     4.7 -val well_ord_iso_subset_lemma = thm "well_ord_iso_subset_lemma";
     4.8  val well_ord_iso_predE = thm "well_ord_iso_predE";
     4.9  val well_ord_iso_pred_eq = thm "well_ord_iso_pred_eq";
    4.10  val ord_iso_image_pred = thm "ord_iso_image_pred";
    4.11  val ord_iso_restrict_pred = thm "ord_iso_restrict_pred";
    4.12  val well_ord_iso_preserving = thm "well_ord_iso_preserving";
    4.13 -val well_ord_iso_unique_lemma = thm "well_ord_iso_unique_lemma";
    4.14  val well_ord_iso_unique = thm "well_ord_iso_unique";
    4.15  val ord_iso_map_subset = thm "ord_iso_map_subset";
    4.16  val domain_ord_iso_map = thm "domain_ord_iso_map";
     5.1 --- a/src/ZF/OrderType.thy	Tue May 28 11:06:55 2002 +0200
     5.2 +++ b/src/ZF/OrderType.thy	Tue May 28 11:07:36 2002 +0200
     5.3 @@ -922,7 +922,6 @@
     5.4  val well_ord_Memrel = thm "well_ord_Memrel";
     5.5  val lt_pred_Memrel = thm "lt_pred_Memrel";
     5.6  val pred_Memrel = thm "pred_Memrel";
     5.7 -val Ord_iso_implies_eq_lemma = thm "Ord_iso_implies_eq_lemma";
     5.8  val Ord_iso_implies_eq = thm "Ord_iso_implies_eq";
     5.9  val ordermap_type = thm "ordermap_type";
    5.10  val ordermap_eq_image = thm "ordermap_eq_image";
    5.11 @@ -996,7 +995,6 @@
    5.12  val Ord_omult = thm "Ord_omult";
    5.13  val pred_Pair_eq = thm "pred_Pair_eq";
    5.14  val ordertype_pred_Pair_eq = thm "ordertype_pred_Pair_eq";
    5.15 -val ordertype_pred_Pair_lemma = thm "ordertype_pred_Pair_lemma";
    5.16  val lt_omult = thm "lt_omult";
    5.17  val omult_oadd_lt = thm "omult_oadd_lt";
    5.18  val omult_unfold = thm "omult_unfold";
     6.1 --- a/src/ZF/Perm.thy	Tue May 28 11:06:55 2002 +0200
     6.2 +++ b/src/ZF/Perm.thy	Tue May 28 11:07:36 2002 +0200
     6.3 @@ -568,10 +568,8 @@
     6.4  val id_bij = thm "id_bij";
     6.5  val subset_iff_id = thm "subset_iff_id";
     6.6  val inj_converse_fun = thm "inj_converse_fun";
     6.7 -val left_inverse_lemma = thm "left_inverse_lemma";
     6.8  val left_inverse = thm "left_inverse";
     6.9  val left_inverse_bij = thm "left_inverse_bij";
    6.10 -val right_inverse_lemma = thm "right_inverse_lemma";
    6.11  val right_inverse = thm "right_inverse";
    6.12  val right_inverse_bij = thm "right_inverse_bij";
    6.13  val inj_converse_inj = thm "inj_converse_inj";
     7.1 --- a/src/ZF/Univ.thy	Tue May 28 11:06:55 2002 +0200
     7.2 +++ b/src/ZF/Univ.thy	Tue May 28 11:07:36 2002 +0200
     7.3 @@ -790,7 +790,6 @@
     7.4  val Pair_in_Vfrom = thm "Pair_in_Vfrom";
     7.5  val succ_in_Vfrom = thm "succ_in_Vfrom";
     7.6  val Vfrom_0 = thm "Vfrom_0";
     7.7 -val Vfrom_succ_lemma = thm "Vfrom_succ_lemma";
     7.8  val Vfrom_succ = thm "Vfrom_succ";
     7.9  val Vfrom_Union = thm "Vfrom_Union";
    7.10  val Limit_Vfrom_eq = thm "Limit_Vfrom_eq";
    7.11 @@ -831,7 +830,6 @@
    7.12  val Vset_succ = thm "Vset_succ";
    7.13  val Transset_Vset = thm "Transset_Vset";
    7.14  val VsetD = thm "VsetD";
    7.15 -val VsetI_lemma = thm "VsetI_lemma";
    7.16  val VsetI = thm "VsetI";
    7.17  val Vset_Ord_rank_iff = thm "Vset_Ord_rank_iff";
    7.18  val Vset_rank_iff = thm "Vset_rank_iff";
    7.19 @@ -868,7 +866,6 @@
    7.20  val Inr_in_univ = thm "Inr_in_univ";
    7.21  val sum_univ = thm "sum_univ";
    7.22  val sum_subset_univ = thm "sum_subset_univ";
    7.23 -val Fin_Vfrom_lemma = thm "Fin_Vfrom_lemma";
    7.24  val Fin_VLimit = thm "Fin_VLimit";
    7.25  val Fin_subset_VLimit = thm "Fin_subset_VLimit";
    7.26  val Fin_univ = thm "Fin_univ";