--- a/src/HOL/Product_Type.thy Wed May 26 16:05:25 2010 +0200
+++ b/src/HOL/Product_Type.thy Wed May 26 16:05:25 2010 +0200
@@ -1147,101 +1147,6 @@
end
*}
-
-subsection {* Legacy bindings *}
-
-ML {*
-val Collect_split = thm "Collect_split";
-val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1";
-val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2";
-val PairE = thm "PairE";
-val Pair_Rep_inject = thm "Pair_Rep_inject";
-val Pair_def = thm "Pair_def";
-val Pair_eq = @{thm "prod.inject"};
-val Pair_fst_snd_eq = thm "Pair_fst_snd_eq";
-val ProdI = thm "ProdI";
-val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq";
-val SigmaD1 = thm "SigmaD1";
-val SigmaD2 = thm "SigmaD2";
-val SigmaE = thm "SigmaE";
-val SigmaE2 = thm "SigmaE2";
-val SigmaI = thm "SigmaI";
-val Sigma_Diff_distrib1 = thm "Sigma_Diff_distrib1";
-val Sigma_Diff_distrib2 = thm "Sigma_Diff_distrib2";
-val Sigma_Int_distrib1 = thm "Sigma_Int_distrib1";
-val Sigma_Int_distrib2 = thm "Sigma_Int_distrib2";
-val Sigma_Un_distrib1 = thm "Sigma_Un_distrib1";
-val Sigma_Un_distrib2 = thm "Sigma_Un_distrib2";
-val Sigma_Union = thm "Sigma_Union";
-val Sigma_def = thm "Sigma_def";
-val Sigma_empty1 = thm "Sigma_empty1";
-val Sigma_empty2 = thm "Sigma_empty2";
-val Sigma_mono = thm "Sigma_mono";
-val The_split = thm "The_split";
-val The_split_eq = thm "The_split_eq";
-val The_split_eq = thm "The_split_eq";
-val Times_Diff_distrib1 = thm "Times_Diff_distrib1";
-val Times_Int_distrib1 = thm "Times_Int_distrib1";
-val Times_Un_distrib1 = thm "Times_Un_distrib1";
-val Times_eq_cancel2 = thm "Times_eq_cancel2";
-val Times_subset_cancel2 = thm "Times_subset_cancel2";
-val UNIV_Times_UNIV = thm "UNIV_Times_UNIV";
-val UN_Times_distrib = thm "UN_Times_distrib";
-val Unity_def = thm "Unity_def";
-val cond_split_eta = thm "cond_split_eta";
-val fst_conv = thm "fst_conv";
-val fst_def = thm "fst_def";
-val fst_eqD = thm "fst_eqD";
-val inj_on_Abs_Prod = thm "inj_on_Abs_Prod";
-val mem_Sigma_iff = thm "mem_Sigma_iff";
-val mem_splitE = thm "mem_splitE";
-val mem_splitI = thm "mem_splitI";
-val mem_splitI2 = thm "mem_splitI2";
-val prod_eqI = thm "prod_eqI";
-val prod_fun = thm "prod_fun";
-val prod_fun_compose = thm "prod_fun_compose";
-val prod_fun_def = thm "prod_fun_def";
-val prod_fun_ident = thm "prod_fun_ident";
-val prod_fun_imageE = thm "prod_fun_imageE";
-val prod_fun_imageI = thm "prod_fun_imageI";
-val prod_induct = thm "prod.induct";
-val snd_conv = thm "snd_conv";
-val snd_def = thm "snd_def";
-val snd_eqD = thm "snd_eqD";
-val split = thm "split";
-val splitD = thm "splitD";
-val splitD' = thm "splitD'";
-val splitE = thm "splitE";
-val splitE' = thm "splitE'";
-val splitE2 = thm "splitE2";
-val splitI = thm "splitI";
-val splitI2 = thm "splitI2";
-val splitI2' = thm "splitI2'";
-val split_beta = thm "split_beta";
-val split_conv = thm "split_conv";
-val split_def = thm "split_def";
-val split_eta = thm "split_eta";
-val split_eta_SetCompr = thm "split_eta_SetCompr";
-val split_eta_SetCompr2 = thm "split_eta_SetCompr2";
-val split_paired_All = thm "split_paired_All";
-val split_paired_Ball_Sigma = thm "split_paired_Ball_Sigma";
-val split_paired_Bex_Sigma = thm "split_paired_Bex_Sigma";
-val split_paired_Ex = thm "split_paired_Ex";
-val split_paired_The = thm "split_paired_The";
-val split_paired_all = thm "split_paired_all";
-val split_part = thm "split_part";
-val split_split = thm "split_split";
-val split_split_asm = thm "split_split_asm";
-val split_tupled_all = thms "split_tupled_all";
-val split_weak_cong = thm "split_weak_cong";
-val surj_pair = thm "surj_pair";
-val surjective_pairing = thm "surjective_pairing";
-val unit_abs_eta_conv = thm "unit_abs_eta_conv";
-val unit_all_eq1 = thm "unit_all_eq1";
-val unit_all_eq2 = thm "unit_all_eq2";
-val unit_eq = thm "unit_eq";
-*}
-
use "Tools/inductive_set.ML"
setup Inductive_Set.setup