diff -r 9caf6883f1f4 -r cd8dbfc272df src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Sun Sep 04 09:49:45 2011 -0700
+++ b/src/HOL/Complex.thy	Sun Sep 04 10:05:52 2011 -0700
@@ -736,12 +736,6 @@
 lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
 by (auto simp add: DeMoivre)
 
-lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
-  by (rule exp_add) (* FIXME: redundant *)
-
-lemma expi_zero: "expi (0::complex) = 1"
-  by (rule exp_zero) (* FIXME: redundant *)
-
 lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
 apply (insert rcis_Ex [of z])
 apply (auto simp add: expi_def rcis_def mult_assoc [symmetric])