(* legacy ML bindings *)
val Iup_def = thm "Iup_def";
val Ifup_def = thm "Ifup_def";
val less_up_def = thm "less_up_def";
val Ifup1 = thm "Ifup1";
val Ifup2 = thm "Ifup2";
val refl_less_up = thm "refl_less_up";
val antisym_less_up = thm "antisym_less_up";
val trans_less_up = thm "trans_less_up";
val minimal_up = thm "minimal_up";
val least_up = thm "least_up";
val monofun_Ifup2 = thm "monofun_Ifup2";
val up_lemma1 = thm "up_lemma1";
val cpo_up = thm "cpo_up";
val up_def = thm "up_def";
val fup_def = thm "fup_def";
val inst_up_pcpo = thm "inst_up_pcpo";
val cont_Iup = thm "cont_Iup";
val cont_Ifup1 = thm "cont_Ifup1";
val cont_Ifup2 = thm "cont_Ifup2";
val Exh_Up1 = thm "Exh_Up1";
val up_inject = thm "up_inject";
val up_eq = thm "up_eq";
val up_defined = thm "up_defined";
val up_less = thm "up_less";
val upE1 = thm "upE1";
val fup1 = thm "fup1";
val fup2 = thm "fup2";
val fup3 = thm "fup3";