# HG changeset patch
# User huffman
# Date 1117150227 -7200
# Node ID c5882ca551ddb3952ddb075082e3b8bc5e6d5df1
# Parent  6aef81a6ddd36f53682f4421f35f339af7689c21
removed obsolete theorems

diff -r 6aef81a6ddd3 -r c5882ca551dd src/HOLCF/Cfun.ML
--- a/src/HOLCF/Cfun.ML	Fri May 27 01:28:51 2005 +0200
+++ b/src/HOLCF/Cfun.ML	Fri May 27 01:30:27 2005 +0200
@@ -5,9 +5,6 @@
 val Rep_Cfun = thm "Rep_Cfun";
 val Rep_Cfun_inverse = thm "Rep_Cfun_inverse";
 val Abs_Cfun_inverse = thm "Abs_Cfun_inverse";
-val refl_less_cfun = thm "refl_less_cfun";
-val antisym_less_cfun = thm "antisym_less_cfun";
-val trans_less_cfun = thm "trans_less_cfun";
 val cfun_cong = thm "cfun_cong";
 val cfun_fun_cong = thm "cfun_fun_cong";
 val cfun_arg_cong = thm "cfun_arg_cong";
@@ -38,7 +35,6 @@
 val cont_lubcfun = thm "cont_lubcfun";
 val lub_cfun = thm "lub_cfun";
 val thelub_cfun = thm "thelub_cfun";
-val cpo_cfun = thm "cpo_cfun";
 val ext_cfun = thm "ext_cfun";
 val semi_monofun_Abs_CFun = thm "semi_monofun_Abs_CFun";
 val less_cfun2 = thm "less_cfun2";