(* legacy ML bindings *) val Abs_CFun_inverse2 = thm "Abs_CFun_inverse2"; val adm_cont = thm "adm_cont"; val assoc_oo = thm "assoc_oo"; val beta_cfun = thm "beta_cfun"; val cfcomp1 = thm "cfcomp1"; val cfcomp2 = thm "cfcomp2"; val cfun_arg_cong = thm "cfun_arg_cong"; val cfun_cong = thm "cfun_cong"; val cfun_fun_cong = thm "cfun_fun_cong"; val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL"; val ch2ch_Rep_CFunR = thm "ch2ch_Rep_CFunR"; val ch2ch_Rep_CFun = thm "ch2ch_Rep_CFun"; val chain_monofun = thm "chain_monofun"; val chfin2chfin = thm "chfin2chfin"; val chfin_Rep_CFunR = thm "chfin_Rep_CFunR"; val cont2cont_LAM = thm "cont2cont_LAM"; val cont2cont_Rep_CFun = thm "cont2cont_Rep_CFun"; val cont2mono_LAM = thm "cont2mono_LAM"; val cont_cfun_arg = thm "cont_cfun_arg"; val cont_cfun_fun = thm "cont_cfun_fun"; val cont_cfun = thm "cont_cfun"; val cont_Istrictify1 = thm "cont_Istrictify1"; val cont_Istrictify2 = thm "cont_Istrictify2"; val cont_lemmas1 = thms "cont_lemmas1"; val contlub_cfun_arg = thm "contlub_cfun_arg"; val contlub_cfun_fun = thm "contlub_cfun_fun"; val cont_lub_cfun = thm "cont_lub_cfun"; val contlub_cfun = thm "contlub_cfun"; val contlub_Istrictify2 = thm "contlub_Istrictify2"; val contlub_Rep_CFun1 = thm "contlub_Rep_CFun1"; val contlub_Rep_CFun2 = thm "contlub_Rep_CFun2"; val cont_Rep_CFun1 = thm "cont_Rep_CFun1"; val cont_Rep_CFun2 = thm "cont_Rep_CFun2"; val eta_cfun = thm "eta_cfun"; val ex_lub_cfun = thm "ex_lub_cfun"; val ext_cfun = thm "ext_cfun"; val flat2flat = thm "flat2flat"; val flat_codom = thm "flat_codom"; val flat_eqI = thm "flat_eqI"; val ID1 = thm "ID1"; val ID2 = thm "ID2"; val ID3 = thm "ID3"; val ID_def = thm "ID_def"; val injection_defined_rev = thm "injection_defined_rev"; val injection_defined = thm "injection_defined"; val injection_eq = thm "injection_eq"; val injection_less = thm "injection_less"; val inst_cfun_pcpo = thm "inst_cfun_pcpo"; val Istrictify1 = thm "Istrictify1"; val Istrictify2 = thm "Istrictify2"; val Istrictify_def = thm "Istrictify_def"; val less_cfun_def = thm "less_CFun_def"; val less_cfun_ext = thm "less_cfun_ext"; val lub_cfun_mono = thm "lub_cfun_mono"; val lub_cfun = thm "lub_cfun"; val monofun_cfun_arg = thm "monofun_cfun_arg"; val monofun_cfun_fun = thm "monofun_cfun_fun"; val monofun_cfun = thm "monofun_cfun"; val monofun_Istrictify2 = thm "monofun_Istrictify2"; val monofun_Rep_CFun1 = thm "monofun_Rep_CFun1"; val monofun_Rep_CFun2 = thm "monofun_Rep_CFun2"; val oo_def = thm "oo_def"; val Rep_CFun_strict1 = thm "Rep_CFun_strict1"; val retraction_strict = thm "retraction_strict"; val semi_monofun_Abs_CFun = thm "semi_monofun_Abs_CFun"; val strictify1 = thm "strictify1"; val strictify2 = thm "strictify2"; val strictify_conv_if = thm "strictify_conv_if"; val strictify_def = thm "strictify_def"; val strictI = thm "strictI"; val thelub_cfun = thm "thelub_cfun"; val UU_CFun = thm "UU_CFun"; structure Cfun = struct val thy = the_context (); val Istrictify_def = Istrictify_def; val strictify_def = strictify_def; val ID_def = ID_def; val oo_def = oo_def; end;