src/HOL/Hyperreal/Poly.thy

--- a/src/HOL/Hyperreal/Poly.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Hyperreal/Poly.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -1026,7 +1026,7 @@
 apply (induct "p", auto)
 apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans)
 apply (rule abs_triangle_ineq)
-apply (auto intro!: mult_mono simp add: abs_mult, arith)
+apply (auto intro!: mult_mono, arith)
 done
 
 ML