# File Up.ML

    (* legacy ML bindings *)

    val antisym_less_up = thm "antisym_less_up";
    val cont_Ifup1 = thm "cont_Ifup1";
    val cont_Ifup2 = thm "cont_Ifup2";
    val cont_Iup = thm "cont_Iup";
    val cpo_up = thm "cpo_up";
    val Exh_Up = thm "Exh_Up";
    val fup1 = thm "fup1";
    val fup2 = thm "fup2";
    val fup3 = thm "fup3";
    val fup_def = thm "fup_def";
    val inst_up_pcpo = thm "inst_up_pcpo";
    val is_lub_Iup = thm "is_lub_Iup";
    val Iup_less = thm "Iup_less";
    val least_up = thm "least_up";
    val less_up_def = thm "less_up_def";
    val minimal_up = thm "minimal_up";
    val monofun_Ifup2 = thm "monofun_Ifup2";
    val not_Iup_less = thm "not_Iup_less";
    val not_up_less_UU = thm "not_up_less_UU";
    val refl_less_up = thm "refl_less_up";
    val trans_less_up = thm "trans_less_up";
    val up_chain_cases = thm "up_chain_cases";
    val up_defined = thm "up_defined";
    val up_def = thm "up_def";
    val up_eq = thm "up_eq";
    val upE = thm "upE";
    val up_inject = thm "up_inject";
    val up_lemma1 = thm "up_lemma1";
    val up_lemma2 = thm "up_lemma2";
    val up_lemma3 = thm "up_lemma3";
    val up_lemma4 = thm "up_lemma4";
    val up_lemma5 = thm "up_lemma5";
    val up_lemma6 = thm "up_lemma6";
    val up_less = thm "up_less";