src/HOL/HOLCF/Cfun.thy

--- a/src/HOL/HOLCF/Cfun.thy	Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/Cfun.thy	Mon Jul 25 21:50:04 2016 +0200
@@ -338,7 +338,7 @@
 text \<open>some lemmata for functions with flat/chfin domain/range types\<close>
 
 lemma chfin_Rep_cfunR: "chain (Y::nat => 'a::cpo->'b::chfin)  
-      ==> !s. ? n. (LUB i. Y i)$s = Y n$s"
+      ==> !s. ? n. (LUB i. Y i)\<cdot>s = Y n\<cdot>s"
 apply (rule allI)
 apply (subst contlub_cfun_fun)
 apply assumption