diff -r defa6fa5fd29 -r 81a4b4a245b0 src/HOLCF/Cprod.ML
--- 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";