diff -r f9243336f54e -r 54018ed3b99d src/HOL/Complex/CLim.thy
--- a/src/HOL/Complex/CLim.thy	Wed Dec 13 20:38:24 2006 +0100
+++ b/src/HOL/Complex/CLim.thy	Wed Dec 13 21:25:56 2006 +0100
@@ -88,12 +88,6 @@
 lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))"
 by transfer (rule refl)
 
-lemma starfun_Re: "( *f* (\<lambda>x. Re (f x))) = (\<lambda>x. hRe (( *f* f) x))"
-by transfer (rule refl)
-
-lemma starfun_Im: "( *f* (\<lambda>x. Im (f x))) = (\<lambda>x. hIm (( *f* f) x))"
-by transfer (rule refl)
-
 lemma star_of_Re [simp]: "star_of (Re x) = hRe (star_of x)"
 by transfer (rule refl)
 
@@ -122,7 +116,7 @@
 apply (auto intro: NSLIM_Re NSLIM_Im)
 apply (auto simp add: NSLIM_def starfun_Re starfun_Im)
 apply (auto dest!: spec)
-apply (simp add: starfunC_approx_Re_Im_iff starfun_Re starfun_Im)
+apply (simp add: hcomplex_approx_iff)
 done
 
 lemma LIM_CRLIM_Re_Im_iff: