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?                *)

     2.1 --- a/src/HOL/NSA/NSComplex.thy	Thu Sep 08 07:06:59 2011 -0700
     2.2 +++ b/src/HOL/NSA/NSComplex.thy	Thu Sep 08 07:16:47 2011 -0700
     2.3 @@ -434,12 +434,6 @@
     2.4  lemma hIm_hsgn [simp]: "!!z. hIm(hsgn z) = hIm(z)/hcmod z"
     2.5  by transfer (rule Im_sgn)
     2.6  
     2.7 -lemma hcomplex_inverse_complex_split:
     2.8 -     "!!x y. inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
     2.9 -      hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
    2.10 -      iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
    2.11 -by transfer (rule complex_inverse_complex_split)
    2.12 -
    2.13  lemma HComplex_inverse:
    2.14       "!!x y. inverse (HComplex x y) =
    2.15        HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"