|
11838
|
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";
|