(* legacy ML bindings *)
val beta_sscase = thm "beta_sscase";
val cont_Iwhen1 = thm "cont_Iwhen1";
val cont_Iwhen2 = thm "cont_Iwhen2";
val cont_Iwhen3 = thm "cont_Iwhen3";
val Exh_Ssum = thm "Exh_Ssum";
val Iwhen1 = thm "Iwhen1";
val Iwhen2 = thm "Iwhen2";
val Iwhen3 = thm "Iwhen3";
val Iwhen4 = thm "Iwhen4";
val Iwhen5 = thm "Iwhen5";
val Iwhen_def = thm "Iwhen_def";
val less_sinlD = thm "less_sinlD";
val less_sinrD = thm "less_sinrD";
val less_ssum_def = thm "less_Ssum_def";
val Rep_Ssum_sinl = thm "Rep_Ssum_sinl";
val Rep_Ssum_sinr = thm "Rep_Ssum_sinr";
val sinl_Abs_Ssum = thm "sinl_Abs_Ssum";
val sinl_defined_iff = thm "sinl_defined_iff";
val sinl_defined = thm "sinl_defined";
val sinl_def = thm "sinl_def";
val sinl_eq_sinr = thm "sinl_eq_sinr";
val sinl_eq = thm "sinl_eq";
val sinl_inject = thm "sinl_inject";
val sinl_less_sinr = thm "sinl_less_sinr";
val sinl_less = thm "sinl_less";
val sinl_strict = thm "sinl_strict";
val sinr_Abs_Ssum = thm "sinr_Abs_Ssum";
val sinr_defined_iff = thm "sinr_defined_iff";
val sinr_defined = thm "sinr_defined";
val sinr_def = thm "sinr_def";
val sinr_eq_sinl = thm "sinr_eq_sinl";
val sinr_eq = thm "sinr_eq";
val sinr_inject = thm "sinr_inject";
val sinr_less_sinl = thm "sinr_less_sinl";
val sinr_less = thm "sinr_less";
val sinr_strict = thm "sinr_strict";
val sscase1 = thm "sscase1";
val sscase2 = thm "sscase2";
val sscase3 = thm "sscase3";
val sscase4 = thm "sscase4";
val sscase_def = thm "sscase_def";
val ssum_chain_lemma = thm "ssum_chain_lemma";
val ssumE2 = thm "ssumE2";
val ssumE = thm "ssumE";
val Ssum_rews = [sinl_strict, sinr_strict, sinl_defined, sinr_defined,
sscase1, sscase2, sscase3];