1.1 --- a/src/HOL/Complex.thy	Thu Sep 08 07:06:59 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Thu Sep 08 07:16:47 2011 -0700
     1.3 @@ -549,12 +549,6 @@
     1.4  lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
     1.5    by (simp add: complex_sgn_def divide_inverse)
     1.6  
     1.7 -lemma complex_inverse_complex_split:
     1.8 -     "inverse(complex_of_real x + ii * complex_of_real y) =
     1.9 -      complex_of_real(x/(x ^ 2 + y ^ 2)) -
    1.10 -      ii * complex_of_real(y/(x ^ 2 + y ^ 2))"
    1.11 -  by (simp add: complex_of_real_def i_def diff_minus divide_inverse)
    1.12 -
    1.13  (*----------------------------------------------------------------------------*)
    1.14  (* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *)
    1.15  (* many of the theorems are not used - so should they be kept?                *)