src/HOL/Hyperreal/Integration.ML

--- a/src/HOL/Hyperreal/Integration.ML	Thu Jan 01 21:47:07 2004 +0100
+++ b/src/HOL/Hyperreal/Integration.ML	Sat Jan 03 16:09:39 2004 +0100
@@ -474,7 +474,7 @@
          (real_mult_le_cancel_iff2 RS iffD1) 2);
 by (Asm_full_simp_tac 2);
 by (asm_full_simp_tac (simpset() 
-     delsimps [abs_inverse]
+     delsimps [abs_inverse, abs_mult]
      addsimps [abs_mult RS sym, real_mult_assoc RS sym]) 2);
 by (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) = \
 \                (f z - f x)/(z - x) - f' x" 2);