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