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