src/HOL/Hyperreal/HTranscendental.thy

 lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
 apply (cases x)
 apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
 apply (rule bexI [OF _ Rep_star_star_n], auto)
 apply (rule_tac x = "exp u" in exI)
-apply (ultra, arith)
+apply ultra
 done
 
 lemma starfun_exp_add_HFinite_Infinitesimal_approx:
      "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x) @= ( *f* exp) z"
 apply (simp add: STAR_exp_add)