diff -r f3bb32a68f16 -r 9449c991cc33 src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Wed May 09 18:25:44 2007 +0200
+++ b/src/HOL/Complex/Complex.thy	Wed May 09 18:26:40 2007 +0200
@@ -474,18 +474,11 @@
   show "z^(Suc n) = z * (z^n)" by simp
 qed
 
-
-lemma complex_of_real_pow: "complex_of_real (x ^ n) = (complex_of_real x) ^ n"
-by (rule of_real_power)
-
 lemma complex_cnj_pow: "cnj(z ^ n) = cnj(z) ^ n"
 apply (induct_tac "n")
 apply (auto simp add: complex_cnj_mult)
 done
 
-lemma complex_mod_complexpow: "cmod(x ^ n) = cmod(x) ^ n"
-by (rule norm_power)
-
 lemma complexpow_i_squared [simp]: "ii ^ 2 = -(1::complex)"
 by (simp add: i_def complex_one_def numeral_2_eq_2)
 
@@ -693,7 +686,7 @@
 done
 
 lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
-by (simp add: rcis_def power_mult_distrib DeMoivre complex_of_real_pow)
+by (simp add: rcis_def power_mult_distrib DeMoivre)
 
 lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
 by (simp add: cis_def complex_inverse_complex_split diff_minus)