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