# HG changeset patch
# User paulson
# Date 1330622034 0
# Node ID 6b94c39b73666755e388a2e857e8d8e7124bb98b
# Parent  b91628b2522b69607a453f5973eb88cedc8dd899
Removal of obsolete ML bindings

diff -r b91628b2522b -r 6b94c39b7366 src/ZF/Bool.thy
--- a/src/ZF/Bool.thy	Thu Mar 01 14:48:32 2012 +0100
+++ b/src/ZF/Bool.thy	Thu Mar 01 17:13:54 2012 +0000
@@ -170,46 +170,4 @@
 lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
 by (simp add: bool_of_o_def)
 
-ML
-{*
-val bool_def = @{thm bool_def};
-val bool_defs = @{thms bool_defs};
-val singleton_0 = @{thm singleton_0};
-val bool_1I = @{thm bool_1I};
-val bool_0I = @{thm bool_0I};
-val one_not_0 = @{thm one_not_0};
-val one_neq_0 = @{thm one_neq_0};
-val boolE = @{thm boolE};
-val cond_1 = @{thm cond_1};
-val cond_0 = @{thm cond_0};
-val cond_type = @{thm cond_type};
-val cond_simple_type = @{thm cond_simple_type};
-val def_cond_1 = @{thm def_cond_1};
-val def_cond_0 = @{thm def_cond_0};
-val not_1 = @{thm not_1};
-val not_0 = @{thm not_0};
-val and_1 = @{thm and_1};
-val and_0 = @{thm and_0};
-val or_1 = @{thm or_1};
-val or_0 = @{thm or_0};
-val xor_1 = @{thm xor_1};
-val xor_0 = @{thm xor_0};
-val not_type = @{thm not_type};
-val and_type = @{thm and_type};
-val or_type = @{thm or_type};
-val xor_type = @{thm xor_type};
-val bool_typechecks = @{thms bool_typechecks};
-val not_not = @{thm not_not};
-val not_and = @{thm not_and};
-val not_or = @{thm not_or};
-val and_absorb = @{thm and_absorb};
-val and_commute = @{thm and_commute};
-val and_assoc = @{thm and_assoc};
-val and_or_distrib = @{thm and_or_distrib};
-val or_absorb = @{thm or_absorb};
-val or_commute = @{thm or_commute};
-val or_assoc = @{thm or_assoc};
-val or_and_distrib = @{thm or_and_distrib};
-*}
-
 end
diff -r b91628b2522b -r 6b94c39b7366 src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Thu Mar 01 14:48:32 2012 +0100
+++ b/src/ZF/Cardinal.thy	Thu Mar 01 17:13:54 2012 +0000
@@ -1042,136 +1042,4 @@
 apply (blast elim: mem_irrefl)
 done
 
-ML
-{*
-val Least_def = @{thm Least_def};
-val eqpoll_def = @{thm eqpoll_def};
-val lepoll_def = @{thm lepoll_def};
-val lesspoll_def = @{thm lesspoll_def};
-val cardinal_def = @{thm cardinal_def};
-val Finite_def = @{thm Finite_def};
-val Card_def = @{thm Card_def};
-val eq_imp_not_mem = @{thm eq_imp_not_mem};
-val decomp_bnd_mono = @{thm decomp_bnd_mono};
-val Banach_last_equation = @{thm Banach_last_equation};
-val decomposition = @{thm decomposition};
-val schroeder_bernstein = @{thm schroeder_bernstein};
-val bij_imp_eqpoll = @{thm bij_imp_eqpoll};
-val eqpoll_refl = @{thm eqpoll_refl};
-val eqpoll_sym = @{thm eqpoll_sym};
-val eqpoll_trans = @{thm eqpoll_trans};
-val subset_imp_lepoll = @{thm subset_imp_lepoll};
-val lepoll_refl = @{thm lepoll_refl};
-val le_imp_lepoll = @{thm le_imp_lepoll};
-val eqpoll_imp_lepoll = @{thm eqpoll_imp_lepoll};
-val lepoll_trans = @{thm lepoll_trans};
-val eqpollI = @{thm eqpollI};
-val eqpollE = @{thm eqpollE};
-val eqpoll_iff = @{thm eqpoll_iff};
-val lepoll_0_is_0 = @{thm lepoll_0_is_0};
-val empty_lepollI = @{thm empty_lepollI};
-val lepoll_0_iff = @{thm lepoll_0_iff};
-val Un_lepoll_Un = @{thm Un_lepoll_Un};
-val eqpoll_0_is_0 = @{thm eqpoll_0_is_0};
-val eqpoll_0_iff = @{thm eqpoll_0_iff};
-val eqpoll_disjoint_Un = @{thm eqpoll_disjoint_Un};
-val lesspoll_not_refl = @{thm lesspoll_not_refl};
-val lesspoll_irrefl = @{thm lesspoll_irrefl};
-val lesspoll_imp_lepoll = @{thm lesspoll_imp_lepoll};
-val lepoll_well_ord = @{thm lepoll_well_ord};
-val lepoll_iff_leqpoll = @{thm lepoll_iff_leqpoll};
-val inj_not_surj_succ = @{thm inj_not_surj_succ};
-val lesspoll_trans = @{thm lesspoll_trans};
-val lesspoll_trans1 = @{thm lesspoll_trans1};
-val lesspoll_trans2 = @{thm lesspoll_trans2};
-val Least_equality = @{thm Least_equality};
-val LeastI = @{thm LeastI};
-val Least_le = @{thm Least_le};
-val less_LeastE = @{thm less_LeastE};
-val LeastI2 = @{thm LeastI2};
-val Least_0 = @{thm Least_0};
-val Ord_Least = @{thm Ord_Least};
-val Least_cong = @{thm Least_cong};
-val cardinal_cong = @{thm cardinal_cong};
-val well_ord_cardinal_eqpoll = @{thm well_ord_cardinal_eqpoll};
-val Ord_cardinal_eqpoll = @{thm Ord_cardinal_eqpoll};
-val well_ord_cardinal_eqE = @{thm well_ord_cardinal_eqE};
-val well_ord_cardinal_eqpoll_iff = @{thm well_ord_cardinal_eqpoll_iff};
-val Ord_cardinal_le = @{thm Ord_cardinal_le};
-val Card_cardinal_eq = @{thm Card_cardinal_eq};
-val CardI = @{thm CardI};
-val Card_is_Ord = @{thm Card_is_Ord};
-val Card_cardinal_le = @{thm Card_cardinal_le};
-val Ord_cardinal = @{thm Ord_cardinal};
-val Card_iff_initial = @{thm Card_iff_initial};
-val lt_Card_imp_lesspoll = @{thm lt_Card_imp_lesspoll};
-val Card_0 = @{thm Card_0};
-val Card_Un = @{thm Card_Un};
-val Card_cardinal = @{thm Card_cardinal};
-val cardinal_mono = @{thm cardinal_mono};
-val cardinal_lt_imp_lt = @{thm cardinal_lt_imp_lt};
-val Card_lt_imp_lt = @{thm Card_lt_imp_lt};
-val Card_lt_iff = @{thm Card_lt_iff};
-val Card_le_iff = @{thm Card_le_iff};
-val well_ord_lepoll_imp_Card_le = @{thm well_ord_lepoll_imp_Card_le};
-val lepoll_cardinal_le = @{thm lepoll_cardinal_le};
-val lepoll_Ord_imp_eqpoll = @{thm lepoll_Ord_imp_eqpoll};
-val lesspoll_imp_eqpoll = @{thm lesspoll_imp_eqpoll};
-val cardinal_subset_Ord = @{thm cardinal_subset_Ord};
-val cons_lepoll_consD = @{thm cons_lepoll_consD};
-val cons_eqpoll_consD = @{thm cons_eqpoll_consD};
-val succ_lepoll_succD = @{thm succ_lepoll_succD};
-val nat_lepoll_imp_le = @{thm nat_lepoll_imp_le};
-val nat_eqpoll_iff = @{thm nat_eqpoll_iff};
-val nat_into_Card = @{thm nat_into_Card};
-val cardinal_0 = @{thm cardinal_0};
-val cardinal_1 = @{thm cardinal_1};
-val succ_lepoll_natE = @{thm succ_lepoll_natE};
-val n_lesspoll_nat = @{thm n_lesspoll_nat};
-val nat_lepoll_imp_ex_eqpoll_n = @{thm nat_lepoll_imp_ex_eqpoll_n};
-val lepoll_imp_lesspoll_succ = @{thm lepoll_imp_lesspoll_succ};
-val lesspoll_succ_imp_lepoll = @{thm lesspoll_succ_imp_lepoll};
-val lesspoll_succ_iff = @{thm lesspoll_succ_iff};
-val lepoll_succ_disj = @{thm lepoll_succ_disj};
-val lesspoll_cardinal_lt = @{thm lesspoll_cardinal_lt};
-val lt_not_lepoll = @{thm lt_not_lepoll};
-val Ord_nat_eqpoll_iff = @{thm Ord_nat_eqpoll_iff};
-val Card_nat = @{thm Card_nat};
-val nat_le_cardinal = @{thm nat_le_cardinal};
-val cons_lepoll_cong = @{thm cons_lepoll_cong};
-val cons_eqpoll_cong = @{thm cons_eqpoll_cong};
-val cons_lepoll_cons_iff = @{thm cons_lepoll_cons_iff};
-val cons_eqpoll_cons_iff = @{thm cons_eqpoll_cons_iff};
-val singleton_eqpoll_1 = @{thm singleton_eqpoll_1};
-val cardinal_singleton = @{thm cardinal_singleton};
-val not_0_is_lepoll_1 = @{thm not_0_is_lepoll_1};
-val succ_eqpoll_cong = @{thm succ_eqpoll_cong};
-val sum_eqpoll_cong = @{thm sum_eqpoll_cong};
-val prod_eqpoll_cong = @{thm prod_eqpoll_cong};
-val inj_disjoint_eqpoll = @{thm inj_disjoint_eqpoll};
-val Diff_sing_lepoll = @{thm Diff_sing_lepoll};
-val lepoll_Diff_sing = @{thm lepoll_Diff_sing};
-val Diff_sing_eqpoll = @{thm Diff_sing_eqpoll};
-val lepoll_1_is_sing = @{thm lepoll_1_is_sing};
-val Un_lepoll_sum = @{thm Un_lepoll_sum};
-val well_ord_Un = @{thm well_ord_Un};
-val disj_Un_eqpoll_sum = @{thm disj_Un_eqpoll_sum};
-val Finite_0 = @{thm Finite_0};
-val lepoll_nat_imp_Finite = @{thm lepoll_nat_imp_Finite};
-val lesspoll_nat_is_Finite = @{thm lesspoll_nat_is_Finite};
-val lepoll_Finite = @{thm lepoll_Finite};
-val subset_Finite = @{thm subset_Finite};
-val Finite_Diff = @{thm Finite_Diff};
-val Finite_cons = @{thm Finite_cons};
-val Finite_succ = @{thm Finite_succ};
-val nat_le_infinite_Ord = @{thm nat_le_infinite_Ord};
-val Finite_imp_well_ord = @{thm Finite_imp_well_ord};
-val nat_wf_on_converse_Memrel = @{thm nat_wf_on_converse_Memrel};
-val nat_well_ord_converse_Memrel = @{thm nat_well_ord_converse_Memrel};
-val well_ord_converse = @{thm well_ord_converse};
-val ordertype_eq_n = @{thm ordertype_eq_n};
-val Finite_well_ord_converse = @{thm Finite_well_ord_converse};
-val nat_into_Finite = @{thm nat_into_Finite};
-*}
-
 end
diff -r b91628b2522b -r 6b94c39b7366 src/ZF/Cardinal_AC.thy
--- a/src/ZF/Cardinal_AC.thy	Thu Mar 01 14:48:32 2012 +0100
+++ b/src/ZF/Cardinal_AC.thy	Thu Mar 01 17:13:54 2012 +0000
@@ -191,10 +191,4 @@
 apply (blast intro!: Ord_UN elim: ltE)
 done
 
-ML
-{*
-val cardinal_0_iff_0 = @{thm cardinal_0_iff_0};
-val cardinal_lt_iff_lesspoll = @{thm cardinal_lt_iff_lesspoll};
-*}
-
 end
diff -r b91628b2522b -r 6b94c39b7366 src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Thu Mar 01 14:48:32 2012 +0100
+++ b/src/ZF/Epsilon.thy	Thu Mar 01 17:13:54 2012 +0000
@@ -396,58 +396,4 @@
      ==> rec(n,a,b) : C(n)"
 by (erule nat_induct, auto)
 
-ML
-{*
-val arg_subset_eclose = @{thm arg_subset_eclose};
-val arg_into_eclose = @{thm arg_into_eclose};
-val Transset_eclose = @{thm Transset_eclose};
-val eclose_subset = @{thm eclose_subset};
-val ecloseD = @{thm ecloseD};
-val arg_in_eclose_sing = @{thm arg_in_eclose_sing};
-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 = @{thm eclose_least};
-val eclose_induct_down = @{thm eclose_induct_down};
-val Transset_eclose_eq_arg = @{thm Transset_eclose_eq_arg};
-val mem_eclose_trans = @{thm mem_eclose_trans};
-val mem_eclose_sing_trans = @{thm mem_eclose_sing_trans};
-val under_Memrel = @{thm under_Memrel};
-val under_Memrel_eclose = @{thm under_Memrel_eclose};
-val wfrec_ssubst = @{thm wfrec_ssubst};
-val wfrec_eclose_eq = @{thm wfrec_eclose_eq};
-val wfrec_eclose_eq2 = @{thm wfrec_eclose_eq2};
-val transrec = @{thm transrec};
-val def_transrec = @{thm def_transrec};
-val transrec_type = @{thm transrec_type};
-val eclose_sing_Ord = @{thm eclose_sing_Ord};
-val Ord_transrec_type = @{thm Ord_transrec_type};
-val rank = @{thm rank};
-val Ord_rank = @{thm Ord_rank};
-val rank_of_Ord = @{thm rank_of_Ord};
-val rank_lt = @{thm rank_lt};
-val eclose_rank_lt = @{thm eclose_rank_lt};
-val rank_mono = @{thm rank_mono};
-val rank_Pow = @{thm rank_Pow};
-val rank_0 = @{thm rank_0};
-val rank_succ = @{thm rank_succ};
-val rank_Union = @{thm rank_Union};
-val rank_eclose = @{thm rank_eclose};
-val rank_pair1 = @{thm rank_pair1};
-val rank_pair2 = @{thm rank_pair2};
-val the_equality_if = @{thm the_equality_if};
-val rank_apply = @{thm rank_apply};
-val mem_eclose_subset = @{thm mem_eclose_subset};
-val eclose_mono = @{thm eclose_mono};
-val eclose_idem = @{thm eclose_idem};
-val transrec2_0 = @{thm transrec2_0};
-val transrec2_succ = @{thm transrec2_succ};
-val transrec2_Limit = @{thm transrec2_Limit};
-val recursor_0 = @{thm recursor_0};
-val recursor_succ = @{thm recursor_succ};
-val rec_0 = @{thm rec_0};
-val rec_succ = @{thm rec_succ};
-val rec_type = @{thm rec_type};
-*}
-
 end
diff -r b91628b2522b -r 6b94c39b7366 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Thu Mar 01 14:48:32 2012 +0100
+++ b/src/ZF/ZF.thy	Thu Mar 01 17:13:54 2012 +0000
@@ -653,15 +653,5 @@
 lemma cantor: "\<exists>S \<in> Pow(A). \<forall>x\<in>A. b(x) ~= S"
 by (best elim!: equalityCE del: ReplaceI RepFun_eqI)
 
-(*Functions for ML scripts*)
-ML
-{*
-(*Converts A<=B to x\<in>A ==> x\<in>B*)
-fun impOfSubs th = th RSN (2, @{thm rev_subsetD});
-
-(*Takes assumptions \<forall>x\<in>A.P(x) and a\<in>A; creates assumption P(a)*)
-val ball_tac = dtac @{thm bspec} THEN' assume_tac
-*}
-
 end