--- a/src/HOLCF/Fun_Cpo.thy Wed Nov 17 12:19:19 2010 -0800
+++ b/src/HOLCF/Fun_Cpo.thy Wed Nov 17 16:05:18 2010 -0800
@@ -46,11 +46,6 @@
subsection {* Full function space is chain complete *}
-text {* Function application is monotone. *}
-
-lemma monofun_app: "monofun (\<lambda>f. f x)"
-by (rule monofunI, simp add: below_fun_def)
-
text {* Properties of chains of functions. *}
lemma fun_chain_iff: "chain S \<longleftrightarrow> (\<forall>x. chain (\<lambda>i. S i x))"
@@ -158,6 +153,9 @@
apply (simp add: cont2contlubE thelub_fun ch2ch_cont)
done
+lemma cont_fun: "cont (\<lambda>f. f x)"
+using cont_id by (rule cont2cont_fun)
+
text {*
Lambda abstraction preserves monotonicity and continuity.
(Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"}.)