--- a/src/HOL/NSA/NSComplex.thy Sat Oct 25 19:20:28 2014 +0200
+++ b/src/HOL/NSA/NSComplex.thy Sun Oct 26 19:11:16 2014 +0100
@@ -374,11 +374,11 @@
lemma hcpow_minus:
"!!x n. (-x::hcomplex) pow n =
(if ( *p* even) n then (x pow n) else -(x pow n))"
-by transfer (rule neg_power_if)
+by transfer simp
lemma hcpow_mult:
"!!r s n. ((r::hcomplex) * s) pow n = (r pow n) * (s pow n)"
-by transfer (rule power_mult_distrib)
+ by (fact hyperpow_mult)
lemma hcpow_zero2 [simp]:
"\<And>n. 0 pow (hSuc n) = (0::'a::{power,semiring_0} star)"