src/HOL/Hyperreal/HLim.thy

--- a/src/HOL/Hyperreal/HLim.thy	Tue May 22 19:58:54 2007 +0200
+++ b/src/HOL/Hyperreal/HLim.thy	Tue May 22 21:32:04 2007 +0200
@@ -106,7 +106,6 @@
 apply (simp add: NSLIM_def)
 apply (rule_tac x="star_of a + of_hypreal epsilon" in exI)
 apply (simp add: hypreal_epsilon_not_zero approx_def)
-apply (rule Infinitesimal_hnorm_iff [THEN iffD1], simp)
 done
 
 lemma NSLIM_not_zero: