# File Ssum.ML

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