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