Removal of obsolete ML bindings
authorpaulson
Thu Mar 01 17:13:54 2012 +0000 (2012-03-01)
changeset 467516b94c39b7366
parent 46747 b91628b2522b
child 46752 e9e7209eb375
Removal of obsolete ML bindings
src/ZF/Bool.thy
src/ZF/Cardinal.thy
src/ZF/Cardinal_AC.thy
src/ZF/Epsilon.thy
src/ZF/ZF.thy
     1.1 --- a/src/ZF/Bool.thy	Thu Mar 01 14:48:32 2012 +0100
     1.2 +++ b/src/ZF/Bool.thy	Thu Mar 01 17:13:54 2012 +0000
     1.3 @@ -170,46 +170,4 @@
     1.4  lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
     1.5  by (simp add: bool_of_o_def)
     1.6  
     1.7 -ML
     1.8 -{*
     1.9 -val bool_def = @{thm bool_def};
    1.10 -val bool_defs = @{thms bool_defs};
    1.11 -val singleton_0 = @{thm singleton_0};
    1.12 -val bool_1I = @{thm bool_1I};
    1.13 -val bool_0I = @{thm bool_0I};
    1.14 -val one_not_0 = @{thm one_not_0};
    1.15 -val one_neq_0 = @{thm one_neq_0};
    1.16 -val boolE = @{thm boolE};
    1.17 -val cond_1 = @{thm cond_1};
    1.18 -val cond_0 = @{thm cond_0};
    1.19 -val cond_type = @{thm cond_type};
    1.20 -val cond_simple_type = @{thm cond_simple_type};
    1.21 -val def_cond_1 = @{thm def_cond_1};
    1.22 -val def_cond_0 = @{thm def_cond_0};
    1.23 -val not_1 = @{thm not_1};
    1.24 -val not_0 = @{thm not_0};
    1.25 -val and_1 = @{thm and_1};
    1.26 -val and_0 = @{thm and_0};
    1.27 -val or_1 = @{thm or_1};
    1.28 -val or_0 = @{thm or_0};
    1.29 -val xor_1 = @{thm xor_1};
    1.30 -val xor_0 = @{thm xor_0};
    1.31 -val not_type = @{thm not_type};
    1.32 -val and_type = @{thm and_type};
    1.33 -val or_type = @{thm or_type};
    1.34 -val xor_type = @{thm xor_type};
    1.35 -val bool_typechecks = @{thms bool_typechecks};
    1.36 -val not_not = @{thm not_not};
    1.37 -val not_and = @{thm not_and};
    1.38 -val not_or = @{thm not_or};
    1.39 -val and_absorb = @{thm and_absorb};
    1.40 -val and_commute = @{thm and_commute};
    1.41 -val and_assoc = @{thm and_assoc};
    1.42 -val and_or_distrib = @{thm and_or_distrib};
    1.43 -val or_absorb = @{thm or_absorb};
    1.44 -val or_commute = @{thm or_commute};
    1.45 -val or_assoc = @{thm or_assoc};
    1.46 -val or_and_distrib = @{thm or_and_distrib};
    1.47 -*}
    1.48 -
    1.49  end
     2.1 --- a/src/ZF/Cardinal.thy	Thu Mar 01 14:48:32 2012 +0100
     2.2 +++ b/src/ZF/Cardinal.thy	Thu Mar 01 17:13:54 2012 +0000
     2.3 @@ -1042,136 +1042,4 @@
     2.4  apply (blast elim: mem_irrefl)
     2.5  done
     2.6  
     2.7 -ML
     2.8 -{*
     2.9 -val Least_def = @{thm Least_def};
    2.10 -val eqpoll_def = @{thm eqpoll_def};
    2.11 -val lepoll_def = @{thm lepoll_def};
    2.12 -val lesspoll_def = @{thm lesspoll_def};
    2.13 -val cardinal_def = @{thm cardinal_def};
    2.14 -val Finite_def = @{thm Finite_def};
    2.15 -val Card_def = @{thm Card_def};
    2.16 -val eq_imp_not_mem = @{thm eq_imp_not_mem};
    2.17 -val decomp_bnd_mono = @{thm decomp_bnd_mono};
    2.18 -val Banach_last_equation = @{thm Banach_last_equation};
    2.19 -val decomposition = @{thm decomposition};
    2.20 -val schroeder_bernstein = @{thm schroeder_bernstein};
    2.21 -val bij_imp_eqpoll = @{thm bij_imp_eqpoll};
    2.22 -val eqpoll_refl = @{thm eqpoll_refl};
    2.23 -val eqpoll_sym = @{thm eqpoll_sym};
    2.24 -val eqpoll_trans = @{thm eqpoll_trans};
    2.25 -val subset_imp_lepoll = @{thm subset_imp_lepoll};
    2.26 -val lepoll_refl = @{thm lepoll_refl};
    2.27 -val le_imp_lepoll = @{thm le_imp_lepoll};
    2.28 -val eqpoll_imp_lepoll = @{thm eqpoll_imp_lepoll};
    2.29 -val lepoll_trans = @{thm lepoll_trans};
    2.30 -val eqpollI = @{thm eqpollI};
    2.31 -val eqpollE = @{thm eqpollE};
    2.32 -val eqpoll_iff = @{thm eqpoll_iff};
    2.33 -val lepoll_0_is_0 = @{thm lepoll_0_is_0};
    2.34 -val empty_lepollI = @{thm empty_lepollI};
    2.35 -val lepoll_0_iff = @{thm lepoll_0_iff};
    2.36 -val Un_lepoll_Un = @{thm Un_lepoll_Un};
    2.37 -val eqpoll_0_is_0 = @{thm eqpoll_0_is_0};
    2.38 -val eqpoll_0_iff = @{thm eqpoll_0_iff};
    2.39 -val eqpoll_disjoint_Un = @{thm eqpoll_disjoint_Un};
    2.40 -val lesspoll_not_refl = @{thm lesspoll_not_refl};
    2.41 -val lesspoll_irrefl = @{thm lesspoll_irrefl};
    2.42 -val lesspoll_imp_lepoll = @{thm lesspoll_imp_lepoll};
    2.43 -val lepoll_well_ord = @{thm lepoll_well_ord};
    2.44 -val lepoll_iff_leqpoll = @{thm lepoll_iff_leqpoll};
    2.45 -val inj_not_surj_succ = @{thm inj_not_surj_succ};
    2.46 -val lesspoll_trans = @{thm lesspoll_trans};
    2.47 -val lesspoll_trans1 = @{thm lesspoll_trans1};
    2.48 -val lesspoll_trans2 = @{thm lesspoll_trans2};
    2.49 -val Least_equality = @{thm Least_equality};
    2.50 -val LeastI = @{thm LeastI};
    2.51 -val Least_le = @{thm Least_le};
    2.52 -val less_LeastE = @{thm less_LeastE};
    2.53 -val LeastI2 = @{thm LeastI2};
    2.54 -val Least_0 = @{thm Least_0};
    2.55 -val Ord_Least = @{thm Ord_Least};
    2.56 -val Least_cong = @{thm Least_cong};
    2.57 -val cardinal_cong = @{thm cardinal_cong};
    2.58 -val well_ord_cardinal_eqpoll = @{thm well_ord_cardinal_eqpoll};
    2.59 -val Ord_cardinal_eqpoll = @{thm Ord_cardinal_eqpoll};
    2.60 -val well_ord_cardinal_eqE = @{thm well_ord_cardinal_eqE};
    2.61 -val well_ord_cardinal_eqpoll_iff = @{thm well_ord_cardinal_eqpoll_iff};
    2.62 -val Ord_cardinal_le = @{thm Ord_cardinal_le};
    2.63 -val Card_cardinal_eq = @{thm Card_cardinal_eq};
    2.64 -val CardI = @{thm CardI};
    2.65 -val Card_is_Ord = @{thm Card_is_Ord};
    2.66 -val Card_cardinal_le = @{thm Card_cardinal_le};
    2.67 -val Ord_cardinal = @{thm Ord_cardinal};
    2.68 -val Card_iff_initial = @{thm Card_iff_initial};
    2.69 -val lt_Card_imp_lesspoll = @{thm lt_Card_imp_lesspoll};
    2.70 -val Card_0 = @{thm Card_0};
    2.71 -val Card_Un = @{thm Card_Un};
    2.72 -val Card_cardinal = @{thm Card_cardinal};
    2.73 -val cardinal_mono = @{thm cardinal_mono};
    2.74 -val cardinal_lt_imp_lt = @{thm cardinal_lt_imp_lt};
    2.75 -val Card_lt_imp_lt = @{thm Card_lt_imp_lt};
    2.76 -val Card_lt_iff = @{thm Card_lt_iff};
    2.77 -val Card_le_iff = @{thm Card_le_iff};
    2.78 -val well_ord_lepoll_imp_Card_le = @{thm well_ord_lepoll_imp_Card_le};
    2.79 -val lepoll_cardinal_le = @{thm lepoll_cardinal_le};
    2.80 -val lepoll_Ord_imp_eqpoll = @{thm lepoll_Ord_imp_eqpoll};
    2.81 -val lesspoll_imp_eqpoll = @{thm lesspoll_imp_eqpoll};
    2.82 -val cardinal_subset_Ord = @{thm cardinal_subset_Ord};
    2.83 -val cons_lepoll_consD = @{thm cons_lepoll_consD};
    2.84 -val cons_eqpoll_consD = @{thm cons_eqpoll_consD};
    2.85 -val succ_lepoll_succD = @{thm succ_lepoll_succD};
    2.86 -val nat_lepoll_imp_le = @{thm nat_lepoll_imp_le};
    2.87 -val nat_eqpoll_iff = @{thm nat_eqpoll_iff};
    2.88 -val nat_into_Card = @{thm nat_into_Card};
    2.89 -val cardinal_0 = @{thm cardinal_0};
    2.90 -val cardinal_1 = @{thm cardinal_1};
    2.91 -val succ_lepoll_natE = @{thm succ_lepoll_natE};
    2.92 -val n_lesspoll_nat = @{thm n_lesspoll_nat};
    2.93 -val nat_lepoll_imp_ex_eqpoll_n = @{thm nat_lepoll_imp_ex_eqpoll_n};
    2.94 -val lepoll_imp_lesspoll_succ = @{thm lepoll_imp_lesspoll_succ};
    2.95 -val lesspoll_succ_imp_lepoll = @{thm lesspoll_succ_imp_lepoll};
    2.96 -val lesspoll_succ_iff = @{thm lesspoll_succ_iff};
    2.97 -val lepoll_succ_disj = @{thm lepoll_succ_disj};
    2.98 -val lesspoll_cardinal_lt = @{thm lesspoll_cardinal_lt};
    2.99 -val lt_not_lepoll = @{thm lt_not_lepoll};
   2.100 -val Ord_nat_eqpoll_iff = @{thm Ord_nat_eqpoll_iff};
   2.101 -val Card_nat = @{thm Card_nat};
   2.102 -val nat_le_cardinal = @{thm nat_le_cardinal};
   2.103 -val cons_lepoll_cong = @{thm cons_lepoll_cong};
   2.104 -val cons_eqpoll_cong = @{thm cons_eqpoll_cong};
   2.105 -val cons_lepoll_cons_iff = @{thm cons_lepoll_cons_iff};
   2.106 -val cons_eqpoll_cons_iff = @{thm cons_eqpoll_cons_iff};
   2.107 -val singleton_eqpoll_1 = @{thm singleton_eqpoll_1};
   2.108 -val cardinal_singleton = @{thm cardinal_singleton};
   2.109 -val not_0_is_lepoll_1 = @{thm not_0_is_lepoll_1};
   2.110 -val succ_eqpoll_cong = @{thm succ_eqpoll_cong};
   2.111 -val sum_eqpoll_cong = @{thm sum_eqpoll_cong};
   2.112 -val prod_eqpoll_cong = @{thm prod_eqpoll_cong};
   2.113 -val inj_disjoint_eqpoll = @{thm inj_disjoint_eqpoll};
   2.114 -val Diff_sing_lepoll = @{thm Diff_sing_lepoll};
   2.115 -val lepoll_Diff_sing = @{thm lepoll_Diff_sing};
   2.116 -val Diff_sing_eqpoll = @{thm Diff_sing_eqpoll};
   2.117 -val lepoll_1_is_sing = @{thm lepoll_1_is_sing};
   2.118 -val Un_lepoll_sum = @{thm Un_lepoll_sum};
   2.119 -val well_ord_Un = @{thm well_ord_Un};
   2.120 -val disj_Un_eqpoll_sum = @{thm disj_Un_eqpoll_sum};
   2.121 -val Finite_0 = @{thm Finite_0};
   2.122 -val lepoll_nat_imp_Finite = @{thm lepoll_nat_imp_Finite};
   2.123 -val lesspoll_nat_is_Finite = @{thm lesspoll_nat_is_Finite};
   2.124 -val lepoll_Finite = @{thm lepoll_Finite};
   2.125 -val subset_Finite = @{thm subset_Finite};
   2.126 -val Finite_Diff = @{thm Finite_Diff};
   2.127 -val Finite_cons = @{thm Finite_cons};
   2.128 -val Finite_succ = @{thm Finite_succ};
   2.129 -val nat_le_infinite_Ord = @{thm nat_le_infinite_Ord};
   2.130 -val Finite_imp_well_ord = @{thm Finite_imp_well_ord};
   2.131 -val nat_wf_on_converse_Memrel = @{thm nat_wf_on_converse_Memrel};
   2.132 -val nat_well_ord_converse_Memrel = @{thm nat_well_ord_converse_Memrel};
   2.133 -val well_ord_converse = @{thm well_ord_converse};
   2.134 -val ordertype_eq_n = @{thm ordertype_eq_n};
   2.135 -val Finite_well_ord_converse = @{thm Finite_well_ord_converse};
   2.136 -val nat_into_Finite = @{thm nat_into_Finite};
   2.137 -*}
   2.138 -
   2.139  end
     3.1 --- a/src/ZF/Cardinal_AC.thy	Thu Mar 01 14:48:32 2012 +0100
     3.2 +++ b/src/ZF/Cardinal_AC.thy	Thu Mar 01 17:13:54 2012 +0000
     3.3 @@ -191,10 +191,4 @@
     3.4  apply (blast intro!: Ord_UN elim: ltE)
     3.5  done
     3.6  
     3.7 -ML
     3.8 -{*
     3.9 -val cardinal_0_iff_0 = @{thm cardinal_0_iff_0};
    3.10 -val cardinal_lt_iff_lesspoll = @{thm cardinal_lt_iff_lesspoll};
    3.11 -*}
    3.12 -
    3.13  end
     4.1 --- a/src/ZF/Epsilon.thy	Thu Mar 01 14:48:32 2012 +0100
     4.2 +++ b/src/ZF/Epsilon.thy	Thu Mar 01 17:13:54 2012 +0000
     4.3 @@ -396,58 +396,4 @@
     4.4       ==> rec(n,a,b) : C(n)"
     4.5  by (erule nat_induct, auto)
     4.6  
     4.7 -ML
     4.8 -{*
     4.9 -val arg_subset_eclose = @{thm arg_subset_eclose};
    4.10 -val arg_into_eclose = @{thm arg_into_eclose};
    4.11 -val Transset_eclose = @{thm Transset_eclose};
    4.12 -val eclose_subset = @{thm eclose_subset};
    4.13 -val ecloseD = @{thm ecloseD};
    4.14 -val arg_in_eclose_sing = @{thm arg_in_eclose_sing};
    4.15 -val arg_into_eclose_sing = @{thm arg_into_eclose_sing};
    4.16 -val eclose_induct = @{thm eclose_induct};
    4.17 -val eps_induct = @{thm eps_induct};
    4.18 -val eclose_least = @{thm eclose_least};
    4.19 -val eclose_induct_down = @{thm eclose_induct_down};
    4.20 -val Transset_eclose_eq_arg = @{thm Transset_eclose_eq_arg};
    4.21 -val mem_eclose_trans = @{thm mem_eclose_trans};
    4.22 -val mem_eclose_sing_trans = @{thm mem_eclose_sing_trans};
    4.23 -val under_Memrel = @{thm under_Memrel};
    4.24 -val under_Memrel_eclose = @{thm under_Memrel_eclose};
    4.25 -val wfrec_ssubst = @{thm wfrec_ssubst};
    4.26 -val wfrec_eclose_eq = @{thm wfrec_eclose_eq};
    4.27 -val wfrec_eclose_eq2 = @{thm wfrec_eclose_eq2};
    4.28 -val transrec = @{thm transrec};
    4.29 -val def_transrec = @{thm def_transrec};
    4.30 -val transrec_type = @{thm transrec_type};
    4.31 -val eclose_sing_Ord = @{thm eclose_sing_Ord};
    4.32 -val Ord_transrec_type = @{thm Ord_transrec_type};
    4.33 -val rank = @{thm rank};
    4.34 -val Ord_rank = @{thm Ord_rank};
    4.35 -val rank_of_Ord = @{thm rank_of_Ord};
    4.36 -val rank_lt = @{thm rank_lt};
    4.37 -val eclose_rank_lt = @{thm eclose_rank_lt};
    4.38 -val rank_mono = @{thm rank_mono};
    4.39 -val rank_Pow = @{thm rank_Pow};
    4.40 -val rank_0 = @{thm rank_0};
    4.41 -val rank_succ = @{thm rank_succ};
    4.42 -val rank_Union = @{thm rank_Union};
    4.43 -val rank_eclose = @{thm rank_eclose};
    4.44 -val rank_pair1 = @{thm rank_pair1};
    4.45 -val rank_pair2 = @{thm rank_pair2};
    4.46 -val the_equality_if = @{thm the_equality_if};
    4.47 -val rank_apply = @{thm rank_apply};
    4.48 -val mem_eclose_subset = @{thm mem_eclose_subset};
    4.49 -val eclose_mono = @{thm eclose_mono};
    4.50 -val eclose_idem = @{thm eclose_idem};
    4.51 -val transrec2_0 = @{thm transrec2_0};
    4.52 -val transrec2_succ = @{thm transrec2_succ};
    4.53 -val transrec2_Limit = @{thm transrec2_Limit};
    4.54 -val recursor_0 = @{thm recursor_0};
    4.55 -val recursor_succ = @{thm recursor_succ};
    4.56 -val rec_0 = @{thm rec_0};
    4.57 -val rec_succ = @{thm rec_succ};
    4.58 -val rec_type = @{thm rec_type};
    4.59 -*}
    4.60 -
    4.61  end
     5.1 --- a/src/ZF/ZF.thy	Thu Mar 01 14:48:32 2012 +0100
     5.2 +++ b/src/ZF/ZF.thy	Thu Mar 01 17:13:54 2012 +0000
     5.3 @@ -653,15 +653,5 @@
     5.4  lemma cantor: "\<exists>S \<in> Pow(A). \<forall>x\<in>A. b(x) ~= S"
     5.5  by (best elim!: equalityCE del: ReplaceI RepFun_eqI)
     5.6  
     5.7 -(*Functions for ML scripts*)
     5.8 -ML
     5.9 -{*
    5.10 -(*Converts A<=B to x\<in>A ==> x\<in>B*)
    5.11 -fun impOfSubs th = th RSN (2, @{thm rev_subsetD});
    5.12 -
    5.13 -(*Takes assumptions \<forall>x\<in>A.P(x) and a\<in>A; creates assumption P(a)*)
    5.14 -val ball_tac = dtac @{thm bspec} THEN' assume_tac
    5.15 -*}
    5.16 -
    5.17  end
    5.18