src/HOL/Product_Type.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 11838 02d75712061d
permissions -rw-r--r--
import -> imports
wenzelm@11838
     1
wenzelm@11838
     2
(* legacy ML bindings *)
wenzelm@11838
     3
wenzelm@11838
     4
val Collect_split = thm "Collect_split";
wenzelm@11838
     5
val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1";
wenzelm@11838
     6
val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2";
wenzelm@11838
     7
val PairE = thm "PairE";
wenzelm@11838
     8
val PairE_lemma = thm "PairE_lemma";
wenzelm@11838
     9
val Pair_Rep_inject = thm "Pair_Rep_inject";
wenzelm@11838
    10
val Pair_def = thm "Pair_def";
wenzelm@11838
    11
val Pair_eq = thm "Pair_eq";
wenzelm@11838
    12
val Pair_fst_snd_eq = thm "Pair_fst_snd_eq";
wenzelm@11838
    13
val Pair_inject = thm "Pair_inject";
wenzelm@11838
    14
val ProdI = thm "ProdI";
wenzelm@11838
    15
val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq";
wenzelm@11838
    16
val SigmaD1 = thm "SigmaD1";
wenzelm@11838
    17
val SigmaD2 = thm "SigmaD2";
wenzelm@11838
    18
val SigmaE = thm "SigmaE";
wenzelm@11838
    19
val SigmaE2 = thm "SigmaE2";
wenzelm@11838
    20
val SigmaI = thm "SigmaI";
wenzelm@11838
    21
val Sigma_Diff_distrib1 = thm "Sigma_Diff_distrib1";
wenzelm@11838
    22
val Sigma_Diff_distrib2 = thm "Sigma_Diff_distrib2";
wenzelm@11838
    23
val Sigma_Int_distrib1 = thm "Sigma_Int_distrib1";
wenzelm@11838
    24
val Sigma_Int_distrib2 = thm "Sigma_Int_distrib2";
wenzelm@11838
    25
val Sigma_Un_distrib1 = thm "Sigma_Un_distrib1";
wenzelm@11838
    26
val Sigma_Un_distrib2 = thm "Sigma_Un_distrib2";
wenzelm@11838
    27
val Sigma_Union = thm "Sigma_Union";
wenzelm@11838
    28
val Sigma_def = thm "Sigma_def";
wenzelm@11838
    29
val Sigma_empty1 = thm "Sigma_empty1";
wenzelm@11838
    30
val Sigma_empty2 = thm "Sigma_empty2";
wenzelm@11838
    31
val Sigma_mono = thm "Sigma_mono";
wenzelm@11838
    32
val The_split = thm "The_split";
wenzelm@11838
    33
val The_split_eq = thm "The_split_eq";
wenzelm@11838
    34
val The_split_eq = thm "The_split_eq";
wenzelm@11838
    35
val Times_Diff_distrib1 = thm "Times_Diff_distrib1";
wenzelm@11838
    36
val Times_Int_distrib1 = thm "Times_Int_distrib1";
wenzelm@11838
    37
val Times_Un_distrib1 = thm "Times_Un_distrib1";
wenzelm@11838
    38
val Times_eq_cancel2 = thm "Times_eq_cancel2";
wenzelm@11838
    39
val Times_subset_cancel2 = thm "Times_subset_cancel2";
wenzelm@11838
    40
val UNIV_Times_UNIV = thm "UNIV_Times_UNIV";
wenzelm@11838
    41
val UN_Times_distrib = thm "UN_Times_distrib";
wenzelm@11838
    42
val Unity_def = thm "Unity_def";
wenzelm@11838
    43
val cond_split_eta = thm "cond_split_eta";
wenzelm@11838
    44
val fst_conv = thm "fst_conv";
wenzelm@11838
    45
val fst_def = thm "fst_def";
wenzelm@11838
    46
val fst_eqD = thm "fst_eqD";
wenzelm@11838
    47
val inj_on_Abs_Prod = thm "inj_on_Abs_Prod";
wenzelm@11838
    48
val injective_fst_snd = thm "injective_fst_snd";
wenzelm@11838
    49
val mem_Sigma_iff = thm "mem_Sigma_iff";
wenzelm@11838
    50
val mem_splitE = thm "mem_splitE";
wenzelm@11838
    51
val mem_splitI = thm "mem_splitI";
wenzelm@11838
    52
val mem_splitI2 = thm "mem_splitI2";
wenzelm@11838
    53
val prod_eqI = thm "prod_eqI";
wenzelm@11838
    54
val prod_fun = thm "prod_fun";
wenzelm@11838
    55
val prod_fun_compose = thm "prod_fun_compose";
wenzelm@11838
    56
val prod_fun_def = thm "prod_fun_def";
wenzelm@11838
    57
val prod_fun_ident = thm "prod_fun_ident";
wenzelm@11838
    58
val prod_fun_imageE = thm "prod_fun_imageE";
wenzelm@11838
    59
val prod_fun_imageI = thm "prod_fun_imageI";
wenzelm@11838
    60
val prod_induct = thm "prod_induct";
wenzelm@11838
    61
val snd_conv = thm "snd_conv";
wenzelm@11838
    62
val snd_def = thm "snd_def";
wenzelm@11838
    63
val snd_eqD = thm "snd_eqD";
wenzelm@11838
    64
val split = thm "split";
wenzelm@11838
    65
val splitD = thm "splitD";
wenzelm@11838
    66
val splitD' = thm "splitD'";
wenzelm@11838
    67
val splitE = thm "splitE";
wenzelm@11838
    68
val splitE' = thm "splitE'";
wenzelm@11838
    69
val splitE2 = thm "splitE2";
wenzelm@11838
    70
val splitI = thm "splitI";
wenzelm@11838
    71
val splitI2 = thm "splitI2";
wenzelm@11838
    72
val splitI2' = thm "splitI2'";
wenzelm@11838
    73
val split_Pair_apply = thm "split_Pair_apply";
wenzelm@11838
    74
val split_beta = thm "split_beta";
wenzelm@11838
    75
val split_conv = thm "split_conv";
wenzelm@11838
    76
val split_def = thm "split_def";
wenzelm@11838
    77
val split_eta = thm "split_eta";
wenzelm@11838
    78
val split_eta_SetCompr = thm "split_eta_SetCompr";
wenzelm@11838
    79
val split_eta_SetCompr2 = thm "split_eta_SetCompr2";
wenzelm@11838
    80
val split_paired_All = thm "split_paired_All";
wenzelm@11838
    81
val split_paired_Ball_Sigma = thm "split_paired_Ball_Sigma";
wenzelm@11838
    82
val split_paired_Bex_Sigma = thm "split_paired_Bex_Sigma";
wenzelm@11838
    83
val split_paired_Ex = thm "split_paired_Ex";
wenzelm@11838
    84
val split_paired_The = thm "split_paired_The";
wenzelm@11838
    85
val split_paired_all = thm "split_paired_all";
wenzelm@11838
    86
val split_part = thm "split_part";
wenzelm@11838
    87
val split_split = thm "split_split";
wenzelm@11838
    88
val split_split_asm = thm "split_split_asm";
wenzelm@11838
    89
val split_tupled_all = thms "split_tupled_all";
wenzelm@11838
    90
val split_weak_cong = thm "split_weak_cong";
wenzelm@11838
    91
val surj_pair = thm "surj_pair";
wenzelm@11838
    92
val surjective_pairing = thm "surjective_pairing";
wenzelm@11838
    93
val unit_abs_eta_conv = thm "unit_abs_eta_conv";
wenzelm@11838
    94
val unit_all_eq1 = thm "unit_all_eq1";
wenzelm@11838
    95
val unit_all_eq2 = thm "unit_all_eq2";
wenzelm@11838
    96
val unit_eq = thm "unit_eq";
wenzelm@11838
    97
val unit_induct = thm "unit_induct";