| author | wenzelm |
| Wed, 13 Jul 2005 16:07:35 +0200 | |
| changeset 16813 | 67140ae50e77 |
| parent 13137 | b642533c7ea4 |
| permissions | -rw-r--r-- |
|
12552
d2d2ab3f1f37
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
diff
changeset
|
1 |
structure Main_ZFC = |
|
d2d2ab3f1f37
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
diff
changeset
|
2 |
struct |
|
d2d2ab3f1f37
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
diff
changeset
|
3 |
val thy = the_context (); |
|
d2d2ab3f1f37
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
diff
changeset
|
4 |
end; |
| 13137 | 5 |
|
6 |
(* legacy ML bindings *) |
|
7 |
||
8 |
(* from AC *) |
|
9 |
val AC_Pi = thm "AC_Pi"; |
|
10 |
val AC_ball_Pi = thm "AC_ball_Pi"; |
|
11 |
val AC_Pi_Pow = thm "AC_Pi_Pow"; |
|
12 |
val AC_func = thm "AC_func"; |
|
13 |
val non_empty_family = thm "non_empty_family"; |
|
14 |
val AC_func0 = thm "AC_func0"; |
|
15 |
val AC_func_Pow = thm "AC_func_Pow"; |
|
16 |
val AC_Pi0 = thm "AC_Pi0"; |
|
17 |
val choice_Diff = thm "choice_Diff"; |
|
18 |
||
19 |
(* from Zorn *) |
|
20 |
val Union_lemma0 = thm "Union_lemma0"; |
|
21 |
val Inter_lemma0 = thm "Inter_lemma0"; |
|
22 |
val increasingD1 = thm "increasingD1"; |
|
23 |
val increasingD2 = thm "increasingD2"; |
|
24 |
val TFin_UnionI = thm "TFin_UnionI"; |
|
25 |
val TFin_is_subset = thm "TFin_is_subset"; |
|
26 |
val TFin_induct = thm "TFin_induct"; |
|
27 |
val increasing_trans = thm "increasing_trans"; |
|
28 |
val TFin_linear_lemma1 = thm "TFin_linear_lemma1"; |
|
29 |
val TFin_linear_lemma2 = thm "TFin_linear_lemma2"; |
|
30 |
val TFin_subsetD = thm "TFin_subsetD"; |
|
31 |
val TFin_subset_linear = thm "TFin_subset_linear"; |
|
32 |
val equal_next_upper = thm "equal_next_upper"; |
|
33 |
val equal_next_Union = thm "equal_next_Union"; |
|
34 |
val chain_subset_Pow = thm "chain_subset_Pow"; |
|
35 |
val super_subset_chain = thm "super_subset_chain"; |
|
36 |
val maxchain_subset_chain = thm "maxchain_subset_chain"; |
|
37 |
val choice_super = thm "choice_super"; |
|
38 |
val choice_not_equals = thm "choice_not_equals"; |
|
39 |
val Hausdorff_next_exists = thm "Hausdorff_next_exists"; |
|
40 |
val TFin_chain_lemma4 = thm "TFin_chain_lemma4"; |
|
41 |
val Hausdorff = thm "Hausdorff"; |
|
42 |
val chain_extend = thm "chain_extend"; |
|
43 |
val Zorn = thm "Zorn"; |
|
44 |
val TFin_well_lemma5 = thm "TFin_well_lemma5"; |
|
45 |
val well_ord_TFin_lemma = thm "well_ord_TFin_lemma"; |
|
46 |
val well_ord_TFin = thm "well_ord_TFin"; |
|
47 |
val Zermelo_next_exists = thm "Zermelo_next_exists"; |
|
48 |
val choice_imp_injection = thm "choice_imp_injection"; |
|
49 |
val AC_well_ord = thm "AC_well_ord"; |
|
50 |
||
51 |
(* from Cardinal_AC *) |
|
52 |
val cardinal_eqpoll = thm "cardinal_eqpoll"; |
|
53 |
val cardinal_idem = thm "cardinal_idem"; |
|
54 |
val cardinal_eqE = thm "cardinal_eqE"; |
|
55 |
val cardinal_eqpoll_iff = thm "cardinal_eqpoll_iff"; |
|
56 |
val cardinal_disjoint_Un = thm "cardinal_disjoint_Un"; |
|
57 |
val lepoll_imp_Card_le = thm "lepoll_imp_Card_le"; |
|
58 |
val cadd_assoc = thm "cadd_assoc"; |
|
59 |
val cmult_assoc = thm "cmult_assoc"; |
|
60 |
val cadd_cmult_distrib = thm "cadd_cmult_distrib"; |
|
61 |
val InfCard_square_eq = thm "InfCard_square_eq"; |
|
62 |
val Card_le_imp_lepoll = thm "Card_le_imp_lepoll"; |
|
63 |
val le_Card_iff = thm "le_Card_iff"; |
|
64 |
val surj_implies_inj = thm "surj_implies_inj"; |
|
65 |
val surj_implies_cardinal_le = thm "surj_implies_cardinal_le"; |
|
66 |
val cardinal_UN_le = thm "cardinal_UN_le"; |
|
67 |
val cardinal_UN_lt_csucc = thm "cardinal_UN_lt_csucc"; |
|
68 |
val cardinal_UN_Ord_lt_csucc = thm "cardinal_UN_Ord_lt_csucc"; |
|
69 |
val inj_UN_subset = thm "inj_UN_subset"; |
|
70 |
val le_UN_Ord_lt_csucc = thm "le_UN_Ord_lt_csucc"; |
|
71 |
||
72 |
(* from InfDatatype *) |
|
73 |
val fun_Limit_VfromE = thm "fun_Limit_VfromE"; |
|
74 |
val fun_Vcsucc_lemma = thm "fun_Vcsucc_lemma"; |
|
75 |
val subset_Vcsucc = thm "subset_Vcsucc"; |
|
76 |
val fun_Vcsucc = thm "fun_Vcsucc"; |
|
77 |
val fun_in_Vcsucc = thm "fun_in_Vcsucc"; |
|
78 |
val fun_in_Vcsucc' = thm "fun_in_Vcsucc'"; |
|
79 |
val Card_fun_Vcsucc = thm "Card_fun_Vcsucc"; |
|
80 |
val Card_fun_in_Vcsucc = thm "Card_fun_in_Vcsucc"; |
|
81 |
val Limit_csucc = thm "Limit_csucc"; |
|
82 |
val Pair_in_Vcsucc = thm "Pair_in_Vcsucc"; |
|
83 |
val Inl_in_Vcsucc = thm "Inl_in_Vcsucc"; |
|
84 |
val Inr_in_Vcsucc = thm "Inr_in_Vcsucc"; |
|
85 |
val zero_in_Vcsucc = thm "zero_in_Vcsucc"; |
|
86 |
val nat_into_Vcsucc = thm "nat_into_Vcsucc"; |
|
87 |
val InfCard_nat_Un_cardinal = thm "InfCard_nat_Un_cardinal"; |
|
88 |
val le_nat_Un_cardinal = thm "le_nat_Un_cardinal"; |
|
89 |
val UN_upper_cardinal = thm "UN_upper_cardinal"; |
|
90 |
||
91 |
val inf_datatype_intrs = thms "inf_datatype_intros"; |
|
92 |