(* legacy ML bindings *) val binchain_cont = thm "binchain_cont"; val ch2ch_cont = thm "ch2ch_cont"; val ch2ch_monofun = thm "ch2ch_monofun"; val chfindom_monofun2cont = thm "chfindom_monofun2cont"; val cont2cont_app2 = thm "cont2cont_app2"; val cont2cont_app3 = thm "cont2cont_app3"; val cont2cont_app = thm "cont2cont_app"; val cont2cont_CF1L_rev = thm "cont2cont_CF1L_rev"; val cont2cont_CF1L = thm "cont2cont_CF1L"; val cont2cont_lambda = thm "cont2cont_lambda"; val cont2contlub_app = thm "cont2contlub_app"; val cont2contlubE = thm "cont2contlubE"; val cont2cont_lub = thm "cont2cont_lub"; val cont2contlub = thm "cont2contlub"; val cont2mono = thm "cont2mono"; val cont_const = thm "cont_const"; val cont_def = thm "cont_def"; val contE = thm "contE"; val cont_finch2finch = thm "cont_finch2finch"; val cont_id = thm "cont_id"; val cont_if = thm "cont_if"; val contI = thm "contI"; val contlub_abstraction = thm "contlub_abstraction"; val contlub_def = thm "contlub_def"; val contlubE = thm "contlubE"; val contlubI = thm "contlubI"; val contlub_lub_fun = thm "contlub_lub_fun"; val flatdom_strict2cont = thm "flatdom_strict2cont"; val flatdom_strict2mono = thm "flatdom_strict2mono"; val mono2mono_app = thm "mono2mono_app"; val mono2mono_MF1L_rev = thm "mono2mono_MF1L_rev"; val mono2mono_MF1L = thm "mono2mono_MF1L"; val monocontlub2cont = thm "monocontlub2cont"; val monofun_def = thm "monofun_def"; val monofunE = thm "monofunE"; val monofun_finch2finch = thm "monofun_finch2finch"; val monofun_fun_arg = thm "monofun_fun_arg"; val monofun_fun_fun = thm "monofun_fun_fun"; val monofun_fun = thm "monofun_fun"; val monofunI = thm "monofunI"; val monofun_lub_fun = thm "monofun_lub_fun"; val ub2ub_monofun = thm "ub2ub_monofun";