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