# HG changeset patch
# User huffman
# Date 1315155952 25200
# Node ID cd8dbfc272df69a8cbc9f1e28c02d68e35a407af
# Parent  9caf6883f1f479fbce58af2a849bb8fa8b9de369
remove redundant lemmas expi_add and expi_zero

diff -r 9caf6883f1f4 -r cd8dbfc272df NEWS
--- 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
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])
diff -r 9caf6883f1f4 -r cd8dbfc272df src/HOL/NSA/NSComplex.thy
--- 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