src/HOL/HOLCF/Cont.thy

--- a/src/HOL/HOLCF/Cont.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/HOLCF/Cont.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -91,7 +91,7 @@
 text {* continuity implies preservation of lubs *}
 
 lemma cont2contlubE:
-  "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion> i. Y i) = (\<Squnion> i. f (Y i))"
+  "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))"
 apply (rule lub_eqI [symmetric])
 apply (erule (1) contE)
 done