--- a/src/HOLCF/Cfun.thy Tue Oct 12 07:46:44 2010 -0700
+++ b/src/HOLCF/Cfun.thy Tue Oct 12 09:08:27 2010 -0700
@@ -316,6 +316,18 @@
using t cont_Rep_CFun2 1 by (rule cont_apply)
qed
+text {*
+ Two specific lemmas for the combination of LCF and HOL terms.
+ These lemmas are needed in theories that use types like @{typ "'a \<rightarrow> 'b \<Rightarrow> 'c"}.
+*}
+
+lemma cont_Rep_CFun_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s)"
+by (rule cont2cont_Rep_CFun [THEN cont2cont_fun])
+
+lemma cont_Rep_CFun_app_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s t)"
+by (rule cont_Rep_CFun_app [THEN cont2cont_fun])
+
+
text {* cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"} *}
lemma cont2mono_LAM:
--- a/src/HOLCF/Lift.thy Tue Oct 12 07:46:44 2010 -0700
+++ b/src/HOLCF/Lift.thy Tue Oct 12 09:08:27 2010 -0700
@@ -86,17 +86,6 @@
by (induct x) auto
qed
-text {*
- \medskip Two specific lemmas for the combination of LCF and HOL
- terms.
-*}
-
-lemma cont_Rep_CFun_app [simp]: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s)"
-by (rule cont2cont_Rep_CFun [THEN cont2cont_fun])
-
-lemma cont_Rep_CFun_app_app [simp]: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s t)"
-by (rule cont_Rep_CFun_app [THEN cont2cont_fun])
-
subsection {* Further operations *}
definition