# HG changeset patch
# User huffman
# Date 1315442489 25200
# Node ID 353ddca2e4c0facd4a6d55182d326b32407d359b
# Parent  34b83d981380eac2232c6eeb716b1331ede0e265
remove redundant lemma complex_of_real_minus_one

diff -r 34b83d981380 -r 353ddca2e4c0 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Wed Sep 07 18:47:55 2011 -0700
+++ b/src/HOL/Complex.thy	Wed Sep 07 17:41:29 2011 -0700
@@ -649,10 +649,6 @@
 lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"
   by (simp add: rcis_def)
 
-lemma complex_of_real_minus_one:
-   "complex_of_real (-(1::real)) = -(1::complex)"
-  by (simp add: complex_of_real_def complex_one_def)
-
 lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
   by (simp add: mult_assoc [symmetric])