diff -r cb34f5f49a08 -r ec32cdaab97b src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Algebra/Lattice.thy	Tue Dec 19 13:58:12 2017 +0100
@@ -52,11 +52,11 @@
 
 definition
   LEAST_FP :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("LFP\<index>") where
-  "LEAST_FP L f = \<Sqinter>\<^bsub>L\<^esub> {u \<in> carrier L. f u \<sqsubseteq>\<^bsub>L\<^esub> u}"    --\<open>least fixed point\<close>
+  "LEAST_FP L f = \<Sqinter>\<^bsub>L\<^esub> {u \<in> carrier L. f u \<sqsubseteq>\<^bsub>L\<^esub> u}"    \<comment>\<open>least fixed point\<close>
 
 definition
   GREATEST_FP:: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("GFP\<index>") where
-  "GREATEST_FP L f = \<Squnion>\<^bsub>L\<^esub> {u \<in> carrier L. u \<sqsubseteq>\<^bsub>L\<^esub> f u}"    --\<open>greatest fixed point\<close>
+  "GREATEST_FP L f = \<Squnion>\<^bsub>L\<^esub> {u \<in> carrier L. u \<sqsubseteq>\<^bsub>L\<^esub> f u}"    \<comment>\<open>greatest fixed point\<close>
 
 
 subsection \<open>Dual operators\<close>