# File Sprod.ML

    (* legacy ML bindings *)

    val eq_sprod = thm "eq_sprod";
    val Exh_Sprod2 = thm "Exh_Sprod2"; (* *)
    val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2"; (* *)
    val less_sprod_def = thm "less_Sprod_def";
    val less_sprod = thm "less_sprod";
    val Rep_Sprod_spair = thm "Rep_Sprod_spair";
    val sfst_defined_iff = thm "sfst_defined_iff";
    val sfst_defined = thm "sfst_defined";
    val sfst_def = thm "sfst_def";
    val sfst_spair = thm "sfst_spair";
    val sfst_strict = thm "sfst_strict";
    val spair_Abs_Sprod = thm "spair_Abs_Sprod";
    val spair_defined_rev = thm "spair_defined_rev";
    val spair_defined = thm "spair_defined";
    val spair_def = thm "spair_def";
    val spair_eq = thm "spair_eq";
    val spair_inject = thm "spair_inject";
    val spair_lemma = thm "spair_lemma";
    val spair_less = thm "spair_less";
    val spair_strict1 = thm "spair_strict1";
    val spair_strict2 = thm "spair_strict2";
    val spair_strict_rev = thm "spair_strict_rev";
    val spair_strict = thm "spair_strict";
    val sprodE = thm "sprodE";
    val ssnd_defined_iff = thm "ssnd_defined_iff";
    val ssnd_defined = thm "ssnd_defined";
    val ssnd_def = thm "ssnd_def";
    val ssnd_spair = thm "ssnd_spair";
    val ssnd_strict = thm "ssnd_strict";
    val ssplit1 = thm "ssplit1";
    val ssplit2 = thm "ssplit2";
    val ssplit3 = thm "ssplit3";
    val ssplit_def = thm "ssplit_def";
    val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2";