diff -r cb34f5f49a08 -r ec32cdaab97b src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Real.thy	Tue Dec 19 13:58:12 2017 +0100
@@ -23,7 +23,7 @@
 
 subsection \<open>Preliminary lemmas\<close>
 
-text{*Useful in convergence arguments*}
+text\<open>Useful in convergence arguments\<close>
 lemma inverse_of_nat_le:
   fixes n::nat shows "\<lbrakk>n \<le> m; n\<noteq>0\<rbrakk> \<Longrightarrow> 1 / of_nat m \<le> (1::'a::linordered_field) / of_nat n"
   by (simp add: frac_le)