# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1493136617 -3600
# Node ID 52eafedaf1966b903cb7167332319f19197d5516
# Parent  e4997c181ccef3dc8b96ddf7ee60933d0189d3ea
Fixed LaTeX issue

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"