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