(*
ID: $Id$
*)
(** legacy ML bindings **)
val all_conj_distrib = thm "all_conj_distrib";
val all_simps = thms "all_simps";
val atomize_not = thm "atomize_not";
val case_split = thm "case_split_thm";
val case_split_thm = thm "case_split_thm"
val cases_simp = thm "cases_simp";
val choice_eq = thm "choice_eq"
val cong = thm "cong"
val conj_comms = thms "conj_comms";
val conj_cong = thm "conj_cong";
val de_Morgan_conj = thm "de_Morgan_conj";
val de_Morgan_disj = thm "de_Morgan_disj";
val disj_assoc = thm "disj_assoc";
val disj_comms = thms "disj_comms";
val disj_cong = thm "disj_cong";
val eq_ac = thms "eq_ac";
val eq_cong2 = thm "eq_cong2"
val Eq_FalseI = thm "Eq_FalseI";
val Eq_TrueI = thm "Eq_TrueI";
val Ex1_def = thm "Ex1_def"
val ex_disj_distrib = thm "ex_disj_distrib";
val ex_simps = thms "ex_simps";
val if_cancel = thm "if_cancel";
val if_eq_cancel = thm "if_eq_cancel";
val if_False = thm "if_False";
val iff_conv_conj_imp = thm "iff_conv_conj_imp";
val iff = thm "iff"
val if_splits = thms "if_splits";
val if_True = thm "if_True";
val if_weak_cong = thm "if_weak_cong"
val imp_all = thm "imp_all";
val imp_cong = thm "imp_cong";
val imp_conjL = thm "imp_conjL";
val imp_conjR = thm "imp_conjR";
val imp_conv_disj = thm "imp_conv_disj";
val simp_implies_def = thm "simp_implies_def";
val simp_thms = thms "simp_thms";
val split_if = thm "split_if";
val the1_equality = thm "the1_equality"
val theI = thm "theI"
val theI' = thm "theI'"
val True_implies_equals = thm "True_implies_equals";