--- a/src/HOL/Hyperreal/NSA.thy Thu Sep 15 23:53:33 2005 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Fri Sep 16 01:34:53 2005 +0200
@@ -1432,9 +1432,8 @@
"[| x < y; u \<in> Infinitesimal |]
==> hypreal_of_real x + u < hypreal_of_real y"
apply (simp add: Infinitesimal_def)
-apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp)
-apply (auto simp add: add_commute abs_less_iff SReal_minus)
-apply (simp add: compare_rls)
+apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp)
+apply (simp add: abs_less_iff)
done
lemma Infinitesimal_add_hrabs_hypreal_of_real_less: