src/HOLCF/Cfun.ML
changeset 16099 c5882ca551dd
parent 16085 c004b9bc970e
child 16209 36ee7f6af79f
--- 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";