--- a/src/HOL/Hyperreal/SEQ.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Tue Oct 05 15:30:50 2004 +0200
@@ -73,7 +73,7 @@
"( *fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfunNat)
apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
-apply (simp add: real_of_nat_Suc_gt_zero abs_eqI2 FreeUltrafilterNat_inverse_real_of_posnat)
+apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
done