(* legacy ML bindings *)
val Iup_def = thm "Iup_def";
val Ifup_def = thm "Ifup_def";
val less_up_def = thm "less_up_def";
val Abs_Up_inverse2 = thm "Abs_Up_inverse2";
val Exh_Up = thm "Exh_Up";
val inj_Abs_Up = thm "inj_Abs_Up";
val inj_Rep_Up = thm "inj_Rep_Up";
val inject_Iup = thm "inject_Iup";
val defined_Iup = thm "defined_Iup";
val upE = thm "upE";
val Ifup1 = thm "Ifup1";
val Ifup2 = thm "Ifup2";
val less_up1a = thm "less_up1a";
val less_up1b = thm "less_up1b";
val less_up1c = thm "less_up1c";
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 inst_up_po = thm "inst_up_po";
val minimal_up = thm "minimal_up";
val UU_up_def = thm "UU_up_def";
val least_up = thm "least_up";
val less_up2b = thm "less_up2b";
val less_up2c = thm "less_up2c";
val monofun_Iup = thm "monofun_Iup";
val monofun_Ifup1 = thm "monofun_Ifup1";
val monofun_Ifup2 = thm "monofun_Ifup2";
val up_lemma1 = thm "up_lemma1";
val lub_up1a = thm "lub_up1a";
val lub_up1b = thm "lub_up1b";
val thelub_up1a = thm "thelub_up1a";
val thelub_up1b = thm "thelub_up1b";
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 less_up3b = thm "less_up3b";
val defined_Iup2 = thm "defined_Iup2";
val contlub_Iup = thm "contlub_Iup";
val cont_Iup = thm "cont_Iup";
val contlub_Ifup1 = thm "contlub_Ifup1";
val contlub_Ifup2 = thm "contlub_Ifup2";
val cont_Ifup1 = thm "cont_Ifup1";
val cont_Ifup2 = thm "cont_Ifup2";
val Exh_Up1 = thm "Exh_Up1";
val inject_up = thm "inject_up";
val defined_up = thm "defined_up";
val upE1 = thm "upE1";
val fup1 = thm "fup1";
val fup2 = thm "fup2";
val less_up4b = thm "less_up4b";
val less_up4c = thm "less_up4c";
val thelub_up2a = thm "thelub_up2a";
val thelub_up2b = thm "thelub_up2b";
val up_lemma2 = thm "up_lemma2";
val thelub_up2a_rev = thm "thelub_up2a_rev";
val thelub_up2b_rev = thm "thelub_up2b_rev";
val thelub_up3 = thm "thelub_up3";
val fup3 = thm "fup3";