--- a/src/HOLCF/Cprod.ML Thu May 26 00:31:48 2005 +0200
+++ b/src/HOLCF/Cprod.ML Thu May 26 02:23:27 2005 +0200
@@ -5,10 +5,7 @@
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 inst_cprod_po = thm "inst_cprod_po";
-val less_cprod4c = thm "less_cprod4c";
val minimal_cprod = thm "minimal_cprod";
-val UU_cprod_def = thm "UU_cprod_def";
val least_cprod = thm "least_cprod";
val monofun_pair1 = thm "monofun_pair1";
val monofun_pair2 = thm "monofun_pair2";
@@ -32,7 +29,6 @@
val contlub_snd = thm "contlub_snd";
val cont_fst = thm "cont_fst";
val cont_snd = thm "cont_snd";
-val beta_cfun_cprod = thm "beta_cfun_cprod";
val inject_cpair = thm "inject_cpair";
val inst_cprod_pcpo2 = thm "inst_cprod_pcpo2";
val defined_cpair_rev = thm "defined_cpair_rev";
@@ -43,7 +39,6 @@
val cfst_strict = thm "cfst_strict";
val csnd_strict = thm "csnd_strict";
val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2";
-val less_cprod5c = thm "less_cprod5c";
val lub_cprod2 = thm "lub_cprod2";
val thelub_cprod2 = thm "thelub_cprod2";
val csplit2 = thm "csplit2";