src/HOL/Complex.thy
changeset 66793 deabce3ccf1f
parent 65583 8d53b3bebab4
child 67082 4e4bea76e559
     1.1 --- a/src/HOL/Complex.thy	Sun Oct 08 16:50:37 2017 +0200
     1.2 +++ b/src/HOL/Complex.thy	Mon Oct 09 15:34:23 2017 +0100
     1.3 @@ -1077,7 +1077,7 @@
     1.4      and Complex_mult_complex_of_real: "Complex x y * complex_of_real r = Complex (x*r) (y*r)"
     1.5      and complex_of_real_mult_Complex: "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
     1.6      and complex_eq_cancel_iff2: "(Complex x y = complex_of_real xa) = (x = xa \<and> y = 0)"
     1.7 -    and complex_cn: "cnj (Complex a b) = Complex a (- b)"
     1.8 +    and complex_cnj: "cnj (Complex a b) = Complex a (- b)"
     1.9      and Complex_sum': "sum (\<lambda>x. Complex (f x) 0) s = Complex (sum f s) 0"
    1.10      and Complex_sum: "Complex (sum f s) 0 = sum (\<lambda>x. Complex (f x) 0) s"
    1.11      and complex_of_real_def: "complex_of_real r = Complex r 0"