src/HOL/Hyperreal/Series.thy
changeset 15003 6145dd7538d7
parent 14416 1f256287d4f0
child 15047 fa62de5862b9
--- a/src/HOL/Hyperreal/Series.thy	Thu Jun 24 17:51:28 2004 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Thu Jun 24 17:52:02 2004 +0200
@@ -506,7 +506,7 @@
 apply (rule_tac x = "abs (f N) * (1/ (1 - c)) / (c ^ N) " in exI)
 apply (rule sums_divide)
 apply (rule sums_mult)
-apply (auto intro!: sums_mult geometric_sums simp add: real_abs_def)
+apply (auto intro!: sums_mult geometric_sums simp add: abs_if)
 done