--- a/src/HOLCF/Lift.thy Sat Nov 05 21:42:24 2005 +0100
+++ b/src/HOLCF/Lift.thy Sat Nov 05 21:50:37 2005 +0100
@@ -103,10 +103,10 @@
*}
lemma cont_Rep_CFun_app: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s)"
-by (rule cont2cont_Rep_CFun [THEN cont2cont_CF1L])
+by (rule cont2cont_Rep_CFun [THEN cont2cont_fun])
lemma cont_Rep_CFun_app_app: "\<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_CF1L])
+by (rule cont_Rep_CFun_app [THEN cont2cont_fun])
subsection {* Further operations *}
@@ -128,7 +128,7 @@
apply (induct x)
apply simp
apply simp
-apply (rule cont_id [THEN cont2cont_CF1L])
+apply (rule cont_id [THEN cont2cont_fun])
done
lemma cont_lift_case2: "cont (\<lambda>x. lift_case \<bottom> f x)"