--- a/src/HOL/Hyperreal/Integration.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Tue Oct 05 15:30:50 2004 +0200
@@ -430,9 +430,9 @@
apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst])
apply (rule add_mono)
apply (rule_tac y = "(e/2) * \<bar>v - x\<bar>" in order_trans)
- prefer 2 apply (simp, arith)
+ prefer 2 apply simp
apply (erule_tac [!] V= "\<forall>x'. x' ~= x & \<bar>x' + - x\<bar> < s --> ?P x'" in thin_rl)
-apply (drule_tac x = v in spec, simp, arith)
+apply (drule_tac x = v in spec, simp)
apply (drule_tac x = u in spec, auto, arith)
apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
apply (rule order_trans)