src/HOL/Product_Type.thy
changeset 37136 e0c9d3e49e15
parent 36664 6302f9ad7047
child 37166 e8400e31528a
     1.1 --- a/src/HOL/Product_Type.thy	Wed May 26 16:05:25 2010 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed May 26 16:05:25 2010 +0200
     1.3 @@ -1147,101 +1147,6 @@
     1.4  end
     1.5  *}
     1.6  
     1.7 -
     1.8 -subsection {* Legacy bindings *}
     1.9 -
    1.10 -ML {*
    1.11 -val Collect_split = thm "Collect_split";
    1.12 -val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1";
    1.13 -val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2";
    1.14 -val PairE = thm "PairE";
    1.15 -val Pair_Rep_inject = thm "Pair_Rep_inject";
    1.16 -val Pair_def = thm "Pair_def";
    1.17 -val Pair_eq = @{thm "prod.inject"};
    1.18 -val Pair_fst_snd_eq = thm "Pair_fst_snd_eq";
    1.19 -val ProdI = thm "ProdI";
    1.20 -val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq";
    1.21 -val SigmaD1 = thm "SigmaD1";
    1.22 -val SigmaD2 = thm "SigmaD2";
    1.23 -val SigmaE = thm "SigmaE";
    1.24 -val SigmaE2 = thm "SigmaE2";
    1.25 -val SigmaI = thm "SigmaI";
    1.26 -val Sigma_Diff_distrib1 = thm "Sigma_Diff_distrib1";
    1.27 -val Sigma_Diff_distrib2 = thm "Sigma_Diff_distrib2";
    1.28 -val Sigma_Int_distrib1 = thm "Sigma_Int_distrib1";
    1.29 -val Sigma_Int_distrib2 = thm "Sigma_Int_distrib2";
    1.30 -val Sigma_Un_distrib1 = thm "Sigma_Un_distrib1";
    1.31 -val Sigma_Un_distrib2 = thm "Sigma_Un_distrib2";
    1.32 -val Sigma_Union = thm "Sigma_Union";
    1.33 -val Sigma_def = thm "Sigma_def";
    1.34 -val Sigma_empty1 = thm "Sigma_empty1";
    1.35 -val Sigma_empty2 = thm "Sigma_empty2";
    1.36 -val Sigma_mono = thm "Sigma_mono";
    1.37 -val The_split = thm "The_split";
    1.38 -val The_split_eq = thm "The_split_eq";
    1.39 -val The_split_eq = thm "The_split_eq";
    1.40 -val Times_Diff_distrib1 = thm "Times_Diff_distrib1";
    1.41 -val Times_Int_distrib1 = thm "Times_Int_distrib1";
    1.42 -val Times_Un_distrib1 = thm "Times_Un_distrib1";
    1.43 -val Times_eq_cancel2 = thm "Times_eq_cancel2";
    1.44 -val Times_subset_cancel2 = thm "Times_subset_cancel2";
    1.45 -val UNIV_Times_UNIV = thm "UNIV_Times_UNIV";
    1.46 -val UN_Times_distrib = thm "UN_Times_distrib";
    1.47 -val Unity_def = thm "Unity_def";
    1.48 -val cond_split_eta = thm "cond_split_eta";
    1.49 -val fst_conv = thm "fst_conv";
    1.50 -val fst_def = thm "fst_def";
    1.51 -val fst_eqD = thm "fst_eqD";
    1.52 -val inj_on_Abs_Prod = thm "inj_on_Abs_Prod";
    1.53 -val mem_Sigma_iff = thm "mem_Sigma_iff";
    1.54 -val mem_splitE = thm "mem_splitE";
    1.55 -val mem_splitI = thm "mem_splitI";
    1.56 -val mem_splitI2 = thm "mem_splitI2";
    1.57 -val prod_eqI = thm "prod_eqI";
    1.58 -val prod_fun = thm "prod_fun";
    1.59 -val prod_fun_compose = thm "prod_fun_compose";
    1.60 -val prod_fun_def = thm "prod_fun_def";
    1.61 -val prod_fun_ident = thm "prod_fun_ident";
    1.62 -val prod_fun_imageE = thm "prod_fun_imageE";
    1.63 -val prod_fun_imageI = thm "prod_fun_imageI";
    1.64 -val prod_induct = thm "prod.induct";
    1.65 -val snd_conv = thm "snd_conv";
    1.66 -val snd_def = thm "snd_def";
    1.67 -val snd_eqD = thm "snd_eqD";
    1.68 -val split = thm "split";
    1.69 -val splitD = thm "splitD";
    1.70 -val splitD' = thm "splitD'";
    1.71 -val splitE = thm "splitE";
    1.72 -val splitE' = thm "splitE'";
    1.73 -val splitE2 = thm "splitE2";
    1.74 -val splitI = thm "splitI";
    1.75 -val splitI2 = thm "splitI2";
    1.76 -val splitI2' = thm "splitI2'";
    1.77 -val split_beta = thm "split_beta";
    1.78 -val split_conv = thm "split_conv";
    1.79 -val split_def = thm "split_def";
    1.80 -val split_eta = thm "split_eta";
    1.81 -val split_eta_SetCompr = thm "split_eta_SetCompr";
    1.82 -val split_eta_SetCompr2 = thm "split_eta_SetCompr2";
    1.83 -val split_paired_All = thm "split_paired_All";
    1.84 -val split_paired_Ball_Sigma = thm "split_paired_Ball_Sigma";
    1.85 -val split_paired_Bex_Sigma = thm "split_paired_Bex_Sigma";
    1.86 -val split_paired_Ex = thm "split_paired_Ex";
    1.87 -val split_paired_The = thm "split_paired_The";
    1.88 -val split_paired_all = thm "split_paired_all";
    1.89 -val split_part = thm "split_part";
    1.90 -val split_split = thm "split_split";
    1.91 -val split_split_asm = thm "split_split_asm";
    1.92 -val split_tupled_all = thms "split_tupled_all";
    1.93 -val split_weak_cong = thm "split_weak_cong";
    1.94 -val surj_pair = thm "surj_pair";
    1.95 -val surjective_pairing = thm "surjective_pairing";
    1.96 -val unit_abs_eta_conv = thm "unit_abs_eta_conv";
    1.97 -val unit_all_eq1 = thm "unit_all_eq1";
    1.98 -val unit_all_eq2 = thm "unit_all_eq2";
    1.99 -val unit_eq = thm "unit_eq";
   1.100 -*}
   1.101 -
   1.102  use "Tools/inductive_set.ML"
   1.103  setup Inductive_Set.setup
   1.104