--- a/src/HOLCF/Cfun.ML Tue Jul 26 18:28:11 2005 +0200
+++ b/src/HOLCF/Cfun.ML Tue Jul 26 18:29:59 2005 +0200
@@ -1,74 +1,78 @@
(* legacy ML bindings *)
-val less_cfun_def = thm "less_CFun_def";
+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 cfun_arg_cong = thm "cfun_arg_cong";
-val Abs_CFun_inverse2 = thm "Abs_CFun_inverse2";
-val beta_cfun = thm "beta_cfun";
-val eta_cfun = thm "eta_cfun";
-val cont_Rep_CFun2 = thm "cont_Rep_CFun2";
-val monofun_Rep_CFun2 = thm "monofun_Rep_CFun2";
-val contlub_Rep_CFun2 = thm "contlub_Rep_CFun2";
-val cont_cfun_arg = thm "cont_cfun_arg";
-val contlub_cfun_arg = thm "contlub_cfun_arg";
-val monofun_Rep_CFun1 = thm "monofun_Rep_CFun1";
-val monofun_cfun_fun = thm "monofun_cfun_fun";
-val monofun_cfun_arg = thm "monofun_cfun_arg";
-val chain_monofun = thm "chain_monofun";
-val monofun_cfun = thm "monofun_cfun";
-val strictI = thm "strictI";
+val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL";
val ch2ch_Rep_CFunR = thm "ch2ch_Rep_CFunR";
-val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL";
-val lub_cfun_mono = thm "lub_cfun_mono";
-val ex_lub_cfun = thm "ex_lub_cfun";
-val cont_lub_cfun = thm "cont_lub_cfun";
-val lub_cfun = thm "lub_cfun";
-val thelub_cfun = thm "thelub_cfun";
-val ext_cfun = thm "ext_cfun";
-val semi_monofun_Abs_CFun = thm "semi_monofun_Abs_CFun";
-val less_cfun_ext = thm "less_cfun_ext";
-val Istrictify_def = thm "Istrictify_def";
-val strictify_def = thm "strictify_def";
-val ID_def = thm "ID_def";
-val oo_def = thm "oo_def";
-val inst_cfun_pcpo = thm "inst_cfun_pcpo";
-val contlub_Rep_CFun1 = thm "contlub_Rep_CFun1";
-val cont_Rep_CFun1 = thm "cont_Rep_CFun1";
-val contlub_cfun_fun = thm "contlub_cfun_fun";
-val cont_cfun_fun = thm "cont_cfun_fun";
-val contlub_cfun = thm "contlub_cfun";
-val cont_cfun = thm "cont_cfun";
+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 cont2cont_LAM = thm "cont2cont_LAM";
-val cont_lemmas1 = [cont_const, cont_id, cont_Rep_CFun2,
- cont2cont_Rep_CFun, cont2cont_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 contlub_Istrictify2 = thm "contlub_Istrictify2";
-val cont_Istrictify1 = thm "cont_Istrictify1";
-val cont_Istrictify2 = thm "cont_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 Rep_CFun_strict1 = thm "Rep_CFun_strict1";
-val chfin_Rep_CFunR = thm "chfin_Rep_CFunR";
-val retraction_strict = thm "retraction_strict";
-val injection_eq = thm "injection_eq";
-val injection_less = thm "injection_less";
-val injection_defined_rev = thm "injection_defined_rev";
-val injection_defined = thm "injection_defined";
-val chfin2chfin = thm "chfin2chfin";
-val flat2flat = thm "flat2flat";
-val flat_codom = thm "flat_codom";
-val ID1 = thm "ID1";
-val cfcomp1 = thm "cfcomp1";
-val cfcomp2 = thm "cfcomp2";
-val ID2 = thm "ID2";
-val ID3 = thm "ID3";
-val assoc_oo = thm "assoc_oo";
+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