Fixed LaTeX issue
authorpaulson <lp15@cam.ac.uk>
Tue Apr 25 17:10:17 2017 +0100 (2017-04-25)
changeset 6557952eafedaf196
parent 65578 e4997c181cce
child 65580 66351f79c295
Fixed LaTeX issue
src/HOL/Complex.thy
     1.1 --- a/src/HOL/Complex.thy	Tue Apr 25 16:39:54 2017 +0100
     1.2 +++ b/src/HOL/Complex.thy	Tue Apr 25 17:10:17 2017 +0100
     1.3 @@ -138,7 +138,7 @@
     1.4  end
     1.5  
     1.6  
     1.7 -subsection \<open>Numerals, Arithmetic, and Embedding from \<real>\<close>
     1.8 +subsection \<open>Numerals, Arithmetic, and Embedding from R\<close>
     1.9  
    1.10  abbreviation complex_of_real :: "real \<Rightarrow> complex"
    1.11    where "complex_of_real \<equiv> of_real"