src/HOL/Complex.thy
changeset 61799 4cf66f21b764
parent 61762 d50b993b4fb9
child 61848 9250e546ab23
     1.1 --- a/src/HOL/Complex.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Complex.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -11,8 +11,8 @@
     1.4  begin
     1.5  
     1.6  text \<open>
     1.7 -We use the @{text codatatype} command to define the type of complex numbers. This allows us to use
     1.8 -@{text primcorec} to define complex functions by defining their real and imaginary result
     1.9 +We use the \<open>codatatype\<close> command to define the type of complex numbers. This allows us to use
    1.10 +\<open>primcorec\<close> to define complex functions by defining their real and imaginary result
    1.11  separately.
    1.12  \<close>
    1.13