--- a/src/HOL/HOLCF/Cont.thy Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/HOLCF/Cont.thy Tue Jan 16 09:30:00 2018 +0100
@@ -18,7 +18,7 @@
subsection \<open>Definitions\<close>
-definition monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" \<comment> "monotonicity"
+definition monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" \<comment> \<open>monotonicity\<close>
where "monofun f \<longleftrightarrow> (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
definition cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"