--- a/src/HOL/Hyperreal/Series.thy Mon May 14 08:15:13 2007 +0200
+++ b/src/HOL/Hyperreal/Series.thy Mon May 14 09:11:30 2007 +0200
@@ -550,7 +550,7 @@
in summable_comparison_test)
apply (rule_tac x = N in exI, safe)
apply (drule le_Suc_ex_iff [THEN iffD1])
-apply (auto simp add: power_add realpow_not_zero)
+apply (auto simp add: power_add field_power_not_zero)
apply (induct_tac "na", auto)
apply (rule_tac y = "c * norm (f (N + n))" in order_trans)
apply (auto intro: mult_right_mono simp add: summable_def)