# HG changeset patch
# User huffman
# Date 1315491407 25200
# Node ID 282eef2c0f7704cfcc385316ee0c0d291dadca05
# Parent  e555032000619adb1f11d3aaf9904a0e39bc460a
remove obsolete intermediate lemma complex_inverse_complex_split

diff -r e55503200061 -r 282eef2c0f77 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Thu Sep 08 07:06:59 2011 -0700
+++ b/src/HOL/Complex.thy	Thu Sep 08 07:16:47 2011 -0700
@@ -549,12 +549,6 @@
 lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
   by (simp add: complex_sgn_def divide_inverse)
 
-lemma complex_inverse_complex_split:
-     "inverse(complex_of_real x + ii * complex_of_real y) =
-      complex_of_real(x/(x ^ 2 + y ^ 2)) -
-      ii * complex_of_real(y/(x ^ 2 + y ^ 2))"
-  by (simp add: complex_of_real_def i_def diff_minus divide_inverse)
-
 (*----------------------------------------------------------------------------*)
 (* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *)
 (* many of the theorems are not used - so should they be kept?                *)
diff -r e55503200061 -r 282eef2c0f77 src/HOL/NSA/NSComplex.thy
--- a/src/HOL/NSA/NSComplex.thy	Thu Sep 08 07:06:59 2011 -0700
+++ b/src/HOL/NSA/NSComplex.thy	Thu Sep 08 07:16:47 2011 -0700
@@ -434,12 +434,6 @@
 lemma hIm_hsgn [simp]: "!!z. hIm(hsgn z) = hIm(z)/hcmod z"
 by transfer (rule Im_sgn)
 
-lemma hcomplex_inverse_complex_split:
-     "!!x y. inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
-      hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
-      iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
-by transfer (rule complex_inverse_complex_split)
-
 lemma HComplex_inverse:
      "!!x y. inverse (HComplex x y) =
       HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"