src/HOL/Hyperreal/NSA.thy

 lemma Infinitesimal_add_hypreal_of_real_less:
      "[| 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 (simp add: abs_less_iff)
+(* FIXME: arith simproc bug with   apply (simp add: abs_less_iff) *)
+apply simp
 done
 
 lemma Infinitesimal_add_hrabs_hypreal_of_real_less:
      "[| x \<in> Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |]
       ==> abs (hypreal_of_real r + x) < hypreal_of_real y"