diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu May 26 17:51:22 2016 +0200
@@ -85,7 +85,7 @@
 where
   "lcm_eucl a b = normalize (a * b) div gcd_eucl a b"
 
-definition Lcm_eucl :: "'a set \<Rightarrow> 'a" -- \<open>
+definition Lcm_eucl :: "'a set \<Rightarrow> 'a" \<comment> \<open>
   Somewhat complicated definition of Lcm that has the advantage of working
   for infinite sets as well\<close>
 where