--- a/NEWS Sun Sep 04 09:49:45 2011 -0700
+++ b/NEWS Sun Sep 04 10:05:52 2011 -0700
@@ -277,6 +277,8 @@
realpow_two_diff ~> square_diff_square_factored
reals_complete2 ~> complete_real
exp_ln_eq ~> ln_unique
+ expi_add ~> exp_add
+ expi_zero ~> exp_zero
lemma_DERIV_subst ~> DERIV_cong
LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff
LIMSEQ_const ~> tendsto_const
--- 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])
--- a/src/HOL/NSA/NSComplex.thy Sun Sep 04 09:49:45 2011 -0700
+++ b/src/HOL/NSA/NSComplex.thy Sun Sep 04 10:05:52 2011 -0700
@@ -613,7 +613,7 @@
by (simp add: NSDeMoivre_ext)
lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)"
-by transfer (rule expi_add)
+by transfer (rule exp_add)
subsection{*@{term hcomplex_of_complex}: the Injection from