--- 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
--- a/src/HOLCF/Cont.ML Tue Jul 26 18:28:11 2005 +0200
+++ b/src/HOLCF/Cont.ML Tue Jul 26 18:29:59 2005 +0200
@@ -1,38 +1,45 @@
(* legacy ML bindings *)
-val monofun_def = thm "monofun_def";
+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 cont_def = thm "cont_def";
+val contlubE = thm "contlubE";
val contlubI = thm "contlubI";
-val contlubE = thm "contlubE";
-val contI = thm "contI";
-val contE = thm "contE";
-val monofunI = thm "monofunI";
+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 ch2ch_monofun = thm "ch2ch_monofun";
-val ub2ub_monofun = thm "ub2ub_monofun";
-val monocontlub2cont = thm "monocontlub2cont";
-val binchain_cont = thm "binchain_cont";
-val cont2mono = thm "cont2mono";
-val cont2contlub = thm "cont2contlub";
val monofun_finch2finch = thm "monofun_finch2finch";
-val cont_finch2finch = thm "cont_finch2finch";
+val monofun_fun_arg = thm "monofun_fun_arg";
val monofun_fun_fun = thm "monofun_fun_fun";
-val monofun_fun_arg = thm "monofun_fun_arg";
-val mono2mono_MF1L = thm "mono2mono_MF1L";
-val cont2cont_CF1L = thm "cont2cont_CF1L";
-val mono2mono_MF1L_rev = thm "mono2mono_MF1L_rev";
-val cont2cont_CF1L_rev = thm "cont2cont_CF1L_rev";
-val cont2cont_lambda = thm "cont2cont_lambda";
-val contlub_abstraction = thm "contlub_abstraction";
-val mono2mono_app = thm "mono2mono_app";
-val cont2contlub_app = thm "cont2contlub_app";
-val cont2cont_app = thm "cont2cont_app";
-val cont2cont_app2 = thm "cont2cont_app2";
-val cont_id = thm "cont_id";
-val cont_const = thm "cont_const";
-val cont2cont_app3 = thm "cont2cont_app3";
-val chfindom_monofun2cont = thm "chfindom_monofun2cont";
-val flatdom_strict2mono = thm "flatdom_strict2mono";
-val flatdom_strict2cont = thm "flatdom_strict2cont";
+val monofun_fun = thm "monofun_fun";
+val monofunI = thm "monofunI";
+val monofun_lub_fun = thm "monofun_lub_fun";
+val ub2ub_monofun = thm "ub2ub_monofun";
--- a/src/HOLCF/Cprod.ML Tue Jul 26 18:28:11 2005 +0200
+++ b/src/HOLCF/Cprod.ML Tue Jul 26 18:29:59 2005 +0200
@@ -1,46 +1,52 @@
(* legacy ML bindings *)
+val antisym_less_cprod = thm "antisym_less_cprod";
+val cfst_cpair = thm "cfst_cpair";
+val cfst_def = thm "cfst_def";
+val cfst_strict = thm "cfst_strict";
+val CLet_def = thm "CLet_def";
+val cont_fst = thm "cont_fst";
+val contlub_fst = thm "contlub_fst";
+val contlub_pair1 = thm "contlub_pair1";
+val contlub_pair2 = thm "contlub_pair2";
+val contlub_snd = thm "contlub_snd";
+val cont_pair1 = thm "cont_pair1";
+val cont_pair2 = thm "cont_pair2";
+val cont_snd = thm "cont_snd";
+val cpair_def = thm "cpair_def";
+val cpair_defined_iff = thm "cpair_defined_iff";
+val cpair_eq_pair = thm "cpair_eq_pair";
+val cpair_eq = thm "cpair_eq";
+val cpair_less = thm "cpair_less";
+val cpo_cprod = thm "cpo_cprod";
+val cprodE = thm "cprodE";
+val Cprod_rews = thms "Cprod_rews";
+val csnd_cpair = thm "csnd_cpair";
+val csnd_def = thm "csnd_def";
+val csnd_strict = thm "csnd_strict";
+val csplit2 = thm "csplit2";
+val csplit3 = thm "csplit3";
+val csplit_def = thm "csplit_def";
+val defined_cpair_rev = thm "defined_cpair_rev";
+val eq_cprod = thm "eq_cprod";
+val Exh_Cprod2 = thm "Exh_Cprod2"; (* rename *)
+val inject_cpair = thm "inject_cpair";
+val inst_cprod_pcpo2 = thm "inst_cprod_pcpo2"; (**)
+val inst_cprod_pcpo = thm "inst_cprod_pcpo";
+val least_cprod = thm "least_cprod";
val less_cprod_def = thm "less_cprod_def";
-val refl_less_cprod = thm "refl_less_cprod";
-val antisym_less_cprod = thm "antisym_less_cprod";
-val trans_less_cprod = thm "trans_less_cprod";
+val less_cprod = thm "less_cprod";
+val lub_cprod2 = thm "lub_cprod2"; (* *)
+val lub_cprod = thm "lub_cprod";
val minimal_cprod = thm "minimal_cprod";
-val least_cprod = thm "least_cprod";
+val monofun_fst = thm "monofun_fst";
val monofun_pair1 = thm "monofun_pair1";
val monofun_pair2 = thm "monofun_pair2";
val monofun_pair = thm "monofun_pair";
-val monofun_fst = thm "monofun_fst";
val monofun_snd = thm "monofun_snd";
-val lub_cprod = thm "lub_cprod";
+val refl_less_cprod = thm "refl_less_cprod";
+val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2"; (* rename *)
+val thelub_cprod2 = thm "thelub_cprod2"; (* *)
val thelub_cprod = thm "thelub_cprod";
-val cpo_cprod = thm "cpo_cprod";
-val cpair_def = thm "cpair_def";
-val cfst_def = thm "cfst_def";
-val csnd_def = thm "csnd_def";
-val csplit_def = thm "csplit_def";
-val CLet_def = thm "CLet_def";
-val inst_cprod_pcpo = thm "inst_cprod_pcpo";
-val contlub_pair1 = thm "contlub_pair1";
-val contlub_pair2 = thm "contlub_pair2";
-val cont_pair1 = thm "cont_pair1";
-val cont_pair2 = thm "cont_pair2";
-val contlub_fst = thm "contlub_fst";
-val contlub_snd = thm "contlub_snd";
-val cont_fst = thm "cont_fst";
-val cont_snd = thm "cont_snd";
-val inject_cpair = thm "inject_cpair";
-val inst_cprod_pcpo2 = thm "inst_cprod_pcpo2";
-val defined_cpair_rev = thm "defined_cpair_rev";
-val Exh_Cprod2 = thm "Exh_Cprod2";
-val cprodE = thm "cprodE";
-val cfst_cpair = thm "cfst_cpair";
-val csnd_cpair = thm "csnd_cpair";
-val cfst_strict = thm "cfst_strict";
-val csnd_strict = thm "csnd_strict";
-val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2";
-val lub_cprod2 = thm "lub_cprod2";
-val thelub_cprod2 = thm "thelub_cprod2";
-val csplit2 = thm "csplit2";
-val csplit3 = thm "csplit3";
-val Cprod_rews = [cfst_cpair, csnd_cpair, csplit2];
+val trans_less_cprod = thm "trans_less_cprod";
--- a/src/HOLCF/Ffun.ML Tue Jul 26 18:28:11 2005 +0200
+++ b/src/HOLCF/Ffun.ML Tue Jul 26 18:29:59 2005 +0200
@@ -1,16 +1,20 @@
(* legacy ML bindings *)
-val less_fun_def = thm "less_fun_def";
-val refl_less_fun = thm "refl_less_fun";
val antisym_less_fun = thm "antisym_less_fun";
-val trans_less_fun = thm "trans_less_fun";
-val minimal_fun = thm "minimal_fun";
-val least_fun = thm "least_fun";
-val less_fun = thm "less_fun";
+val app_strict = thm "app_strict";
val ch2ch_fun = thm "ch2ch_fun";
-val ub2ub_fun = thm "ub2ub_fun";
-val lub_fun = thm "lub_fun";
-val thelub_fun = thm "thelub_fun";
+val ch2ch_fun_rev = thm "ch2ch_fun_rev";
val cpo_fun = thm "cpo_fun";
val inst_fun_pcpo = thm "inst_fun_pcpo";
+val least_fun = thm "least_fun";
+val less_fun_def = thm "less_fun_def";
+val less_fun_ext = thm "less_fun_ext";
+val less_fun = thm "less_fun";
+val lub_fun = thm "lub_fun";
+val minimal_fun = thm "minimal_fun";
+val refl_less_fun = thm "refl_less_fun";
+val thelub_fun = thm "thelub_fun";
+val trans_less_fun = thm "trans_less_fun";
+val ub2ub_fun = thm "ub2ub_fun";
+
--- a/src/HOLCF/Fix.ML Tue Jul 26 18:28:11 2005 +0200
+++ b/src/HOLCF/Fix.ML Tue Jul 26 18:29:59 2005 +0200
@@ -1,36 +1,41 @@
(* legacy ML bindings *)
-val iterate_0 = thm "iterate_0";
-val iterate_Suc = thm "iterate_Suc";
-val Ifix_def = thm "Ifix_def";
-val fix_def = thm "fix_def";
+val adm_chfindom = thm "adm_chfindom";
+val adm_impl_admw = thm "adm_impl_admw";
val admw_def = thm "admw_def";
-val iterate_Suc2 = thm "iterate_Suc2";
val chain_iterate2 = thm "chain_iterate2";
val chain_iterate = thm "chain_iterate";
-val Ifix_eq = thm "Ifix_eq";
-val Ifix_least = thm "Ifix_least";
+val cont_Ifix = thm "cont_Ifix";
val cont_iterate1 = thm "cont_iterate1";
val cont_iterate2 = thm "cont_iterate2";
-val monofun_iterate2 = thm "monofun_iterate2";
+val cont_iterate = thm "cont_iterate";
val contlub_iterate2 = thm "contlub_iterate2";
-val cont_iterate = thm "cont_iterate";
-val cont_Ifix = thm "cont_Ifix";
-val fix_eq = thm "fix_eq";
-val fix_least = thm "fix_least";
-val fix_eqI = thm "fix_eqI";
+val def_fix_ind = thm "def_fix_ind";
+val def_wfix_ind = thm "def_wfix_ind";
+val fix_const = thm "fix_const";
+val fix_def2 = thm "fix_def2";
+val fix_defined = thm "fix_defined";
+val fix_defined_iff = thm "fix_defined_iff";
+val fix_def = thm "fix_def";
val fix_eq2 = thm "fix_eq2";
val fix_eq3 = thm "fix_eq3";
val fix_eq4 = thm "fix_eq4";
val fix_eq5 = thm "fix_eq5";
-val fix_def2 = thm "fix_def2";
-val def_fix_ind = thm "def_fix_ind";
-val adm_impl_admw = thm "adm_impl_admw";
+val fix_eqI = thm "fix_eqI";
+val fix_eq = thm "fix_eq";
+val fix_id = thm "fix_id";
val fix_ind = thm "fix_ind";
-val def_fix_ind = thm "def_fix_ind";
+val fix_least = thm "fix_least";
+val fix_strict = thm "fix_strict";
+val Ifix_def = thm "Ifix_def";
+val Ifix_eq = thm "Ifix_eq";
+val Ifix_least = thm "Ifix_least";
+val iterate_0 = thm "iterate_0";
+val iterate_Suc2 = thm "iterate_Suc2";
+val iterate_Suc = thm "iterate_Suc";
+val monofun_iterate2 = thm "monofun_iterate2";
val wfix_ind = thm "wfix_ind";
-val def_wfix_ind = thm "def_wfix_ind";
structure Fix =
struct
--- a/src/HOLCF/Lift.ML Tue Jul 26 18:28:11 2005 +0200
+++ b/src/HOLCF/Lift.ML Tue Jul 26 18:29:59 2005 +0200
@@ -15,24 +15,35 @@
val size = thms "lift.size";
end;
-val Def_not_UU = thm "Def_not_UU";
+val cont2cont_flift1 = thm "cont2cont_flift1";
+val cont2cont_lift_case = thm "cont2cont_lift_case";
+val cont_flift1 = thm "cont_flift1";
+val cont_lemmas_ext = thms "cont_lemmas_ext";
+val cont_lift_case1 = thm "cont_lift_case1";
+val cont_lift_case2 = thm "cont_lift_case2";
+val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app";
+val cont_Rep_CFun_app = thm "cont_Rep_CFun_app";
+val DefE2 = thm "DefE2";
val DefE = thm "DefE";
-val DefE2 = thm "DefE2";
val Def_inject_less_eq = thm "Def_inject_less_eq";
+val Def_inject = thm "Def_inject";
val Def_less_is_eq = thm "Def_less_is_eq";
-val Lift_cases = thm "Lift_cases";
-val Lift_exhaust = thm "Lift_exhaust";
-val cont_Rep_CFun_app = thm "cont_Rep_CFun_app";
-val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app";
-val cont_if = thm "cont_if";
+val Def_not_UU = thm "Def_not_UU";
+val flift1_def = thm "flift1_def";
val flift1_Def = thm "flift1_Def";
val flift1_strict = thm "flift1_strict";
-val flift1_def = thm "flift1_def";
+val flift2_defined = thm "flift2_defined";
+val flift2_def = thm "flift2_def";
val flift2_Def = thm "flift2_Def";
val flift2_strict = thm "flift2_strict";
-val flift2_def = thm "flift2_def";
-val flift2_defined = thm "flift2_defined";
+val inst_lift_pcpo = thm "inst_lift_pcpo";
+val less_lift_def = thm "less_lift_def";
val less_lift = thm "less_lift";
-val less_lift_def = thm "less_lift_def";
+val Lift_cases = thm "Lift_cases";
+val lift_definedE = thm "lift_definedE";
+val lift_distinct1 = thm "lift_distinct1";
+val lift_distinct2 = thm "lift_distinct2";
+val Lift_exhaust = thm "Lift_exhaust";
+val lift_induct = thm "lift_induct";
val liftpair_def = thm "liftpair_def";
val not_Undef_is_Def = thm "not_Undef_is_Def";
--- a/src/HOLCF/One.ML Tue Jul 26 18:28:11 2005 +0200
+++ b/src/HOLCF/One.ML Tue Jul 26 18:29:59 2005 +0200
@@ -1,7 +1,7 @@
(* legacy ML bindings *)
+val dist_eq_one = thms "dist_eq_one";
+val dist_less_one = thm "dist_less_one";
val Exh_one = thm "Exh_one";
val oneE = thm "oneE";
-val dist_less_one = thm "dist_less_one";
-val dist_eq_one = thms "dist_eq_one";
--- a/src/HOLCF/Pcpo.ML Tue Jul 26 18:28:11 2005 +0200
+++ b/src/HOLCF/Pcpo.ML Tue Jul 26 18:29:59 2005 +0200
@@ -1,36 +1,41 @@
(* legacy ML bindings *)
-val cpo = thm "cpo";
-val least = thm "least";
-val UU_def = thm "UU_def";
+val ax_flat = thm "ax_flat";
+val ch2ch_lub = thm "ch2ch_lub";
+val chain_mono2 = thm "chain_mono2";
+val chain_UU_I_inverse2 = thm "chain_UU_I_inverse2";
+val chain_UU_I_inverse = thm "chain_UU_I_inverse";
+val chain_UU_I = thm "chain_UU_I";
+val chfin2finch = thm "chfin2finch";
+val chfin_imp_cpo = thm "chfin_imp_cpo";
val chfin = thm "chfin";
-val ax_flat = thm "ax_flat";
-val UU_least = thm "UU_least";
-val minimal = thm "minimal";
-val thelubE = thm "thelubE";
+val cpo = thm "cpo";
+val diag_lub = thm "diag_lub";
+val eq_UU_iff = thm "eq_UU_iff";
+val ex_lub = thm "ex_lub";
+val flat_eq = thm "flat_eq";
+val flat_imp_chfin = thm "flat_imp_chfin";
+val increasing_chain_adm_lemma = thm "increasing_chain_adm_lemma";
+val infinite_chain_adm_lemma = thm "infinite_chain_adm_lemma";
+val is_lub_thelub = thm "is_lub_thelub";
val is_ub_thelub = thm "is_ub_thelub";
-val is_lub_thelub = thm "is_lub_thelub";
-val lub_range_shift = thm "lub_range_shift";
-val maxinch_is_thelub = thm "maxinch_is_thelub";
-val lub_mono = thm "lub_mono";
+val least = thm "least";
+val lub_equal2 = thm "lub_equal2";
val lub_equal = thm "lub_equal";
val lub_mono2 = thm "lub_mono2";
-val lub_equal2 = thm "lub_equal2";
val lub_mono3 = thm "lub_mono3";
-val eq_UU_iff = thm "eq_UU_iff";
-val UU_I = thm "UU_I";
+val lub_mono = thm "lub_mono";
+val lub_range_shift = thm "lub_range_shift";
+val maxinch_is_thelub = thm "maxinch_is_thelub";
+val minimal = thm "minimal";
val not_less2not_eq = thm "not_less2not_eq";
-val chain_UU_I = thm "chain_UU_I";
-val chain_UU_I_inverse = thm "chain_UU_I_inverse";
-val chain_UU_I_inverse2 = thm "chain_UU_I_inverse2";
val notUU_I = thm "notUU_I";
-val chain_mono2 = thm "chain_mono2";
-val flat_imp_chfin = thm "flat_imp_chfin";
-val flat_eq = thm "flat_eq";
-val chfin2finch = thm "chfin2finch";
-val infinite_chain_adm_lemma = thm "infinite_chain_adm_lemma";
-val increasing_chain_adm_lemma = thm "increasing_chain_adm_lemma";
+val thelubE = thm "thelubE";
+val UU_def = thm "UU_def";
+val UU_I = thm "UU_I";
+val UU_least = thm "UU_least";
+val UU_reorient = thm "UU_reorient";
structure Pcpo =
struct
--- a/src/HOLCF/Porder.ML Tue Jul 26 18:28:11 2005 +0200
+++ b/src/HOLCF/Porder.ML Tue Jul 26 18:29:59 2005 +0200
@@ -1,44 +1,46 @@
(* legacy ML bindings *)
-val refl_less = thm "refl_less";
+val antisym_less_inverse = thm "antisym_less_inverse";
val antisym_less = thm "antisym_less";
-val trans_less = thm "trans_less";
-val minimal2UU = thm "minimal2UU";
-val antisym_less_inverse = thm "antisym_less_inverse";
+val bin_chainmax = thm "bin_chainmax";
+val bin_chain = thm "bin_chain";
val box_less = thm "box_less";
-val po_eq_conv = thm "po_eq_conv";
-val is_ub_def = thm "is_ub_def";
-val is_lub_def = thm "is_lub_def";
-val tord_def = thm "tord_def";
val chain_def = thm "chain_def";
-val max_in_chain_def = thm "max_in_chain_def";
-val finite_chain_def = thm "finite_chain_def";
-val lub_def = thm "lub_def";
-val unique_lub = thm "unique_lub";
-val chain_mono = thm "chain_mono";
-val chain_mono3 = thm "chain_mono3";
-val chain_tord = thm "chain_tord";
-val lub = thm "lub";
-val lubI = thm "lubI";
-val thelubI = thm "thelubI";
-val lub_singleton = thm "lub_singleton";
-val is_lubD1 = thm "is_lubD1";
-val is_lub_lub = thm "is_lub_lub";
-val is_lubI = thm "is_lubI";
val chainE = thm "chainE";
val chainI = thm "chainI";
+val chain_mono3 = thm "chain_mono3";
+val chain_mono = thm "chain_mono";
val chain_shift = thm "chain_shift";
-val ub_rangeD = thm "ub_rangeD";
-val ub_rangeI = thm "ub_rangeI";
+val chain_tord = thm "chain_tord";
+val finite_chain_def = thm "finite_chain_def";
+val is_lubD1 = thm "is_lubD1";
+val is_lub_def = thm "is_lub_def";
+val is_lubI = thm "is_lubI";
+val is_lub_lub = thm "is_lub_lub";
+val is_lub_range_shift = thm "is_lub_range_shift";
+val is_ub_def = thm "is_ub_def";
val is_ub_lub = thm "is_ub_lub";
-val lub_finch1 = thm "lub_finch1";
-val lub_finch2 = thm "lub_finch2";
-val bin_chain = thm "bin_chain";
-val bin_chainmax = thm "bin_chainmax";
+val is_ub_range_shift = thm "is_ub_range_shift";
val lub_bin_chain = thm "lub_bin_chain";
val lub_chain_maxelem = thm "lub_chain_maxelem";
val lub_const = thm "lub_const";
+val lub_def = thm "lub_def";
+val lub_finch1 = thm "lub_finch1";
+val lub_finch2 = thm "lub_finch2";
+val lubI = thm "lubI";
+val lub_singleton = thm "lub_singleton";
+val lub = thm "lub";
+val max_in_chain_def = thm "max_in_chain_def";
+val minimal2UU = thm "minimal2UU";
+val po_eq_conv = thm "po_eq_conv";
+val refl_less = thm "refl_less";
+val thelubI = thm "thelubI";
+val tord_def = thm "tord_def";
+val trans_less = thm "trans_less";
+val ub_rangeD = thm "ub_rangeD";
+val ub_rangeI = thm "ub_rangeI";
+val unique_lub = thm "unique_lub";
structure Porder =
struct
--- a/src/HOLCF/Sprod.ML Tue Jul 26 18:28:11 2005 +0200
+++ b/src/HOLCF/Sprod.ML Tue Jul 26 18:29:59 2005 +0200
@@ -1,32 +1,37 @@
(* legacy ML bindings *)
+val eq_sprod = thm "eq_sprod";
+val Exh_Sprod2 = thm "Exh_Sprod2"; (* *)
+val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2"; (* *)
val less_sprod_def = thm "less_Sprod_def";
-val spair_def = thm "spair_def";
+val less_sprod = thm "less_sprod";
+val Rep_Sprod_spair = thm "Rep_Sprod_Spair";
+val sfst_defined_iff = thm "sfst_defined_iff";
+val sfst_defined = thm "sfst_defined";
val sfst_def = thm "sfst_def";
-val ssnd_def = thm "ssnd_def";
-val ssplit_def = thm "ssplit_def";
-val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2";
-val spair_strict = thm "spair_strict";
+val sfst_spair = thm "sfst_spair";
+val sfst_strict = thm "sfst_strict";
+val spair_Abs_Sprod = thm "spair_Abs_Sprod";
+val spair_defined_rev = thm "spair_defined_rev";
+val spair_defined = thm "spair_defined";
+val spair_def = thm "spair_def";
+val spair_eq = thm "spair_eq";
+val spair_inject = thm "spair_inject";
+val spair_lemma = thm "spair_lemma";
+val spair_less = thm "spair_less";
val spair_strict1 = thm "spair_strict1";
val spair_strict2 = thm "spair_strict2";
val spair_strict_rev = thm "spair_strict_rev";
-val spair_defined_rev = thm "spair_defined_rev";
-val spair_defined = thm "spair_defined";
-val spair_eq = thm "spair_eq";
-val spair_inject = thm "spair_inject";
-val Exh_Sprod2 = thm "Exh_Sprod2";
+val spair_strict = thm "spair_strict";
val sprodE = thm "sprodE";
-val sfst_strict = thm "sfst_strict";
+val ssnd_defined_iff = thm "ssnd_defined_iff";
+val ssnd_defined = thm "ssnd_defined";
+val ssnd_def = thm "ssnd_def";
+val ssnd_spair = thm "ssnd_spair";
val ssnd_strict = thm "ssnd_strict";
-val sfst_spair = thm "sfst_spair";
-val ssnd_spair = thm "ssnd_spair";
-val sfst_defined = thm "sfst_defined";
-val ssnd_defined = thm "ssnd_defined";
-val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2";
-val less_sprod = thm "less_sprod";
-val spair_less = thm "spair_less";
val ssplit1 = thm "ssplit1";
val ssplit2 = thm "ssplit2";
val ssplit3 = thm "ssplit3";
-
+val ssplit_def = thm "ssplit_def";
+val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2";
--- a/src/HOLCF/Ssum.ML Tue Jul 26 18:28:11 2005 +0200
+++ b/src/HOLCF/Ssum.ML Tue Jul 26 18:29:59 2005 +0200
@@ -1,35 +1,49 @@
(* legacy ML bindings *)
-val Iwhen_def = thm "Iwhen_def";
-val Iwhen1 = thm "Iwhen1";
-val Iwhen2 = thm "Iwhen2";
-val Iwhen3 = thm "Iwhen3";
-val less_ssum_def = thm "less_Ssum_def";
-val sinl_def = thm "sinl_def";
-val sinr_def = thm "sinr_def";
-val sscase_def = thm "sscase_def";
+val beta_sscase = thm "beta_sscase";
val cont_Iwhen1 = thm "cont_Iwhen1";
val cont_Iwhen2 = thm "cont_Iwhen2";
val cont_Iwhen3 = thm "cont_Iwhen3";
-val sinl_strict = thm "sinl_strict";
-val sinr_strict = thm "sinr_strict";
+val Exh_Ssum = thm "Exh_Ssum";
+val Iwhen1 = thm "Iwhen1";
+val Iwhen2 = thm "Iwhen2";
+val Iwhen3 = thm "Iwhen3";
+val Iwhen4 = thm "Iwhen4";
+val Iwhen5 = thm "Iwhen5";
+val Iwhen_def = thm "Iwhen_def";
+val less_sinlD = thm "less_sinlD";
+val less_sinrD = thm "less_sinrD";
+val less_ssum_def = thm "less_Ssum_def";
+val Rep_Ssum_sinl = thm "Rep_Ssum_sinl";
+val Rep_Ssum_sinr = thm "Rep_Ssum_sinr";
+val sinl_Abs_Ssum = thm "sinl_Abs_Ssum";
+val sinl_defined_iff = thm "sinl_defined_iff";
+val sinl_defined = thm "sinl_defined";
+val sinl_def = thm "sinl_def";
+val sinl_eq_sinr = thm "sinl_eq_sinr";
+val sinl_eq = thm "sinl_eq";
val sinl_inject = thm "sinl_inject";
-val sinr_inject = thm "sinr_inject";
-val sinl_eq = thm "sinl_eq";
-val sinr_eq = thm "sinr_eq";
-val sinl_defined = thm "sinl_defined";
+val sinl_less_sinr = thm "sinl_less_sinr";
+val sinl_less = thm "sinl_less";
+val sinl_strict = thm "sinl_strict";
+val sinr_Abs_Ssum = thm "sinr_Abs_Ssum";
+val sinr_defined_iff = thm "sinr_defined_iff";
val sinr_defined = thm "sinr_defined";
-val Exh_Ssum1 = thm "Exh_Ssum1";
-val ssumE = thm "ssumE";
-val ssumE2 = thm "ssumE2";
-val sinl_less = thm "sinl_less";
+val sinr_def = thm "sinr_def";
+val sinr_eq_sinl = thm "sinr_eq_sinl";
+val sinr_eq = thm "sinr_eq";
+val sinr_inject = thm "sinr_inject";
+val sinr_less_sinl = thm "sinr_less_sinl";
val sinr_less = thm "sinr_less";
-val sinl_less_sinr = thm "sinl_less_sinr";
-val sinr_less_sinl = thm "sinr_less_sinl";
+val sinr_strict = thm "sinr_strict";
val sscase1 = thm "sscase1";
val sscase2 = thm "sscase2";
val sscase3 = thm "sscase3";
val sscase4 = thm "sscase4";
+val sscase_def = thm "sscase_def";
+val ssum_chain_lemma = thm "ssum_chain_lemma";
+val ssumE2 = thm "ssumE2";
+val ssumE = thm "ssumE";
val Ssum_rews = [sinl_strict, sinr_strict, sinl_defined, sinr_defined,
sscase1, sscase2, sscase3];
--- a/src/HOLCF/Tr.ML Tue Jul 26 18:28:11 2005 +0200
+++ b/src/HOLCF/Tr.ML Tue Jul 26 18:29:59 2005 +0200
@@ -1,33 +1,32 @@
(* legacy ML bindings *)
-val TT_def = thm "TT_def";
-val FF_def = thm "FF_def";
-val neg_def = thm "neg_def";
-val ifte_def = thm "ifte_def";
+val adm_nFF = thm "adm_nFF";
+val adm_nTT = thm "adm_nTT";
+val adm_trick_1 = thm "adm_trick_1";
+val adm_trick_2 = thm "adm_trick_2";
+val adm_tricks = thms "adm_tricks";
+val andalso_and = thm "andalso_and";
val andalso_def = thm "andalso_def";
-val orelse_def = thm "orelse_def";
-val If2_def = thm "If2_def";
-val Exh_tr = thm "Exh_tr";
-val trE = thm "trE";
-val tr_defs = thms "tr_defs";
-val dist_less_tr = thms "dist_less_tr";
-val dist_eq_tr = thms "dist_eq_tr";
-val ifte_thms = thms "ifte_thms";
+val andalso_or = thm "andalso_or";
val andalso_thms = thms "andalso_thms";
-val orelse_thms = thms "orelse_thms";
-val neg_thms = thms "neg_thms";
-val split_If2 = thm "split_If2";
-val andalso_or = thm "andalso_or";
-val andalso_and = thm "andalso_and";
val Def_bool1 = thm "Def_bool1";
val Def_bool2 = thm "Def_bool2";
val Def_bool3 = thm "Def_bool3";
val Def_bool4 = thm "Def_bool4";
+val dist_eq_tr = thms "dist_eq_tr";
+val dist_less_tr = thms "dist_less_tr";
+val Exh_tr = thm "Exh_tr";
+val FF_def = thm "FF_def";
+val If2_def = thm "If2_def";
val If_and_if = thm "If_and_if";
-val adm_trick_1 = thm "adm_trick_1";
-val adm_trick_2 = thm "adm_trick_2";
-val adm_tricks = thms "adm_tricks";
-val adm_nTT = thm "adm_nTT";
-val adm_nFF = thm "adm_nFF";
-
+val ifte_def = thm "ifte_def";
+val ifte_thms = thms "ifte_thms";
+val neg_def = thm "neg_def";
+val neg_thms = thms "neg_thms";
+val orelse_def = thm "orelse_def";
+val orelse_thms = thms "orelse_thms";
+val split_If2 = thm "split_If2";
+val tr_defs = thms "tr_defs";
+val trE = thm "trE";
+val TT_def = thm "TT_def";
--- a/src/HOLCF/Up.ML Tue Jul 26 18:28:11 2005 +0200
+++ b/src/HOLCF/Up.ML Tue Jul 26 18:29:59 2005 +0200
@@ -1,27 +1,38 @@
(* legacy ML bindings *)
-val less_up_def = thm "less_up_def";
-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 minimal_up = thm "minimal_up";
-val least_up = thm "least_up";
-val monofun_Ifup2 = thm "monofun_Ifup2";
-val up_lemma1 = thm "up_lemma1";
-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 cont_Iup = thm "cont_Iup";
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 up_inject = thm "up_inject";
-val up_eq = thm "up_eq";
-val up_defined = thm "up_defined";
-val up_less = thm "up_less";
-val upE = thm "upE";
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";
+