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