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