structure Main_ZFC =
struct
val thy = the_context ();
end;
(* legacy ML bindings *)
(* from AC *)
val AC_Pi = thm "AC_Pi";
val AC_ball_Pi = thm "AC_ball_Pi";
val AC_Pi_Pow = thm "AC_Pi_Pow";
val AC_func = thm "AC_func";
val non_empty_family = thm "non_empty_family";
val AC_func0 = thm "AC_func0";
val AC_func_Pow = thm "AC_func_Pow";
val AC_Pi0 = thm "AC_Pi0";
val choice_Diff = thm "choice_Diff";
(* from Zorn *)
val Union_lemma0 = thm "Union_lemma0";
val Inter_lemma0 = thm "Inter_lemma0";
val increasingD1 = thm "increasingD1";
val increasingD2 = thm "increasingD2";
val TFin_UnionI = thm "TFin_UnionI";
val TFin_is_subset = thm "TFin_is_subset";
val TFin_induct = thm "TFin_induct";
val increasing_trans = thm "increasing_trans";
val TFin_linear_lemma1 = thm "TFin_linear_lemma1";
val TFin_linear_lemma2 = thm "TFin_linear_lemma2";
val TFin_subsetD = thm "TFin_subsetD";
val TFin_subset_linear = thm "TFin_subset_linear";
val equal_next_upper = thm "equal_next_upper";
val equal_next_Union = thm "equal_next_Union";
val chain_subset_Pow = thm "chain_subset_Pow";
val super_subset_chain = thm "super_subset_chain";
val maxchain_subset_chain = thm "maxchain_subset_chain";
val choice_super = thm "choice_super";
val choice_not_equals = thm "choice_not_equals";
val Hausdorff_next_exists = thm "Hausdorff_next_exists";
val TFin_chain_lemma4 = thm "TFin_chain_lemma4";
val Hausdorff = thm "Hausdorff";
val chain_extend = thm "chain_extend";
val Zorn = thm "Zorn";
val TFin_well_lemma5 = thm "TFin_well_lemma5";
val well_ord_TFin_lemma = thm "well_ord_TFin_lemma";
val well_ord_TFin = thm "well_ord_TFin";
val Zermelo_next_exists = thm "Zermelo_next_exists";
val choice_imp_injection = thm "choice_imp_injection";
val AC_well_ord = thm "AC_well_ord";
(* from Cardinal_AC *)
val cardinal_eqpoll = thm "cardinal_eqpoll";
val cardinal_idem = thm "cardinal_idem";
val cardinal_eqE = thm "cardinal_eqE";
val cardinal_eqpoll_iff = thm "cardinal_eqpoll_iff";
val cardinal_disjoint_Un = thm "cardinal_disjoint_Un";
val lepoll_imp_Card_le = thm "lepoll_imp_Card_le";
val cadd_assoc = thm "cadd_assoc";
val cmult_assoc = thm "cmult_assoc";
val cadd_cmult_distrib = thm "cadd_cmult_distrib";
val InfCard_square_eq = thm "InfCard_square_eq";
val Card_le_imp_lepoll = thm "Card_le_imp_lepoll";
val le_Card_iff = thm "le_Card_iff";
val surj_implies_inj = thm "surj_implies_inj";
val surj_implies_cardinal_le = thm "surj_implies_cardinal_le";
val cardinal_UN_le = thm "cardinal_UN_le";
val cardinal_UN_lt_csucc = thm "cardinal_UN_lt_csucc";
val cardinal_UN_Ord_lt_csucc = thm "cardinal_UN_Ord_lt_csucc";
val inj_UN_subset = thm "inj_UN_subset";
val le_UN_Ord_lt_csucc = thm "le_UN_Ord_lt_csucc";
(* from InfDatatype *)
val fun_Limit_VfromE = thm "fun_Limit_VfromE";
val fun_Vcsucc_lemma = thm "fun_Vcsucc_lemma";
val subset_Vcsucc = thm "subset_Vcsucc";
val fun_Vcsucc = thm "fun_Vcsucc";
val fun_in_Vcsucc = thm "fun_in_Vcsucc";
val fun_in_Vcsucc' = thm "fun_in_Vcsucc'";
val Card_fun_Vcsucc = thm "Card_fun_Vcsucc";
val Card_fun_in_Vcsucc = thm "Card_fun_in_Vcsucc";
val Limit_csucc = thm "Limit_csucc";
val Pair_in_Vcsucc = thm "Pair_in_Vcsucc";
val Inl_in_Vcsucc = thm "Inl_in_Vcsucc";
val Inr_in_Vcsucc = thm "Inr_in_Vcsucc";
val zero_in_Vcsucc = thm "zero_in_Vcsucc";
val nat_into_Vcsucc = thm "nat_into_Vcsucc";
val InfCard_nat_Un_cardinal = thm "InfCard_nat_Un_cardinal";
val le_nat_Un_cardinal = thm "le_nat_Un_cardinal";
val UN_upper_cardinal = thm "UN_upper_cardinal";
val inf_datatype_intrs = thms "inf_datatype_intros";