--- a/src/HOL/Hyperreal/Lim.thy Sat Dec 09 18:06:17 2006 +0100
+++ b/src/HOL/Hyperreal/Lim.thy Sun Dec 10 07:12:26 2006 +0100
@@ -966,7 +966,7 @@
and aux: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (X x - L) < r"
by fast
from LIMSEQ_D [OF S sgz]
- obtain no where "\<forall>n\<ge>no. norm (S n - a) < s" by fast
+ obtain no where "\<forall>n\<ge>no. norm (S n - a) < s" by blast
hence "\<forall>n\<ge>no. norm (X (S n) - L) < r" by (simp add: aux as)
thus "\<exists>no. \<forall>n\<ge>no. norm (X (S n) - L) < r" ..
qed