# File Tr.ML

    (* 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";