--- a/src/HOL/NSA/NSComplex.thy Wed Sep 07 10:04:07 2011 -0700
+++ b/src/HOL/NSA/NSComplex.thy Wed Sep 07 18:47:55 2011 -0700
@@ -561,8 +561,7 @@
"!!a. hcis (hypreal_of_nat (Suc n) * a) =
hcis a * hcis (hypreal_of_nat n * a)"
apply transfer
-apply (fold real_of_nat_def)
-apply (rule cis_real_of_nat_Suc_mult)
+apply (simp add: left_distrib cis_mult)
done
lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)"
@@ -574,7 +573,7 @@
lemma hcis_hypreal_of_hypnat_Suc_mult:
"!! a n. hcis (hypreal_of_hypnat (n + 1) * a) =
hcis a * hcis (hypreal_of_hypnat n * a)"
-by transfer (fold real_of_nat_def, simp add: cis_real_of_nat_Suc_mult)
+by transfer (simp add: left_distrib cis_mult)
lemma NSDeMoivre_ext:
"!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)"