diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Library/Float.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -639,7 +639,7 @@
 end
 
 
-subsection \<open>Lemmas for types @{typ real}, @{typ nat}, @{typ int}\<close>
+subsection \<open>Lemmas for types \<^typ>\<open>real\<close>, \<^typ>\<open>nat\<close>, \<^typ>\<open>int\<close>\<close>
 
 lemmas real_of_ints =
   of_int_add