(* legacy ML bindings *) val adm_nFF = thm "adm_nFF"; val adm_nTT = thm "adm_nTT"; val adm_trick_1 = thm "adm_trick_1"; val adm_trick_2 = thm "adm_trick_2"; val adm_tricks = thms "adm_tricks"; val andalso_and = thm "andalso_and"; val andalso_def = thm "andalso_def"; val andalso_or = thm "andalso_or"; val andalso_thms = thms "andalso_thms"; val Def_bool1 = thm "Def_bool1"; val Def_bool2 = thm "Def_bool2"; val Def_bool3 = thm "Def_bool3"; val Def_bool4 = thm "Def_bool4"; val dist_eq_tr = thms "dist_eq_tr"; val dist_less_tr = thms "dist_less_tr"; val Exh_tr = thm "Exh_tr"; val FF_def = thm "FF_def"; val If2_def = thm "If2_def"; val If_and_if = thm "If_and_if"; val ifte_def = thm "ifte_def"; val ifte_thms = thms "ifte_thms"; val neg_def = thm "neg_def"; val neg_thms = thms "neg_thms"; val orelse_def = thm "orelse_def"; val orelse_thms = thms "orelse_thms"; val split_If2 = thm "split_If2"; val tr_defs = thms "tr_defs"; val trE = thm "trE"; val TT_def = thm "TT_def";