remove redundant lemma complex_of_real_minus_one
authorhuffman
Wed Sep 07 17:41:29 2011 -0700 (2011-09-07)
changeset 44825353ddca2e4c0
parent 44824 34b83d981380
child 44826 1120cba9bce4
remove redundant lemma complex_of_real_minus_one
src/HOL/Complex.thy
     1.1 --- a/src/HOL/Complex.thy	Wed Sep 07 18:47:55 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Wed Sep 07 17:41:29 2011 -0700
     1.3 @@ -649,10 +649,6 @@
     1.4  lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"
     1.5    by (simp add: rcis_def)
     1.6  
     1.7 -lemma complex_of_real_minus_one:
     1.8 -   "complex_of_real (-(1::real)) = -(1::complex)"
     1.9 -  by (simp add: complex_of_real_def complex_one_def)
    1.10 -
    1.11  lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
    1.12    by (simp add: mult_assoc [symmetric])
    1.13