# HG changeset patch
# User huffman
# Date 1286899707 25200
# Node ID 58ead6f77f8e00271cc7853c45d69d39f7162c96
# Parent  bb04a995bbd3661a168e2398fd2b857ba5f0a1ae
move lemmas from Lift.thy to Cfun.thy

diff -r bb04a995bbd3 -r 58ead6f77f8e src/HOLCF/Cfun.thy
--- 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:
diff -r bb04a995bbd3 -r 58ead6f77f8e src/HOLCF/Lift.thy
--- 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