diff -r e4997c181cce -r 52eafedaf196 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Apr 25 16:39:54 2017 +0100
+++ b/src/HOL/Complex.thy	Tue Apr 25 17:10:17 2017 +0100
@@ -138,7 +138,7 @@
 end
 
 
-subsection \<open>Numerals, Arithmetic, and Embedding from \<real>\<close>
+subsection \<open>Numerals, Arithmetic, and Embedding from R\<close>
 
 abbreviation complex_of_real :: "real \<Rightarrow> complex"
   where "complex_of_real \<equiv> of_real"