diff -r 3eae3140b4b2 -r 496b42cf588d src/HOL/Hyperreal/Lim.thy --- a/src/HOL/Hyperreal/Lim.thy Sat May 19 04:51:03 2007 +0200 +++ b/src/HOL/Hyperreal/Lim.thy Sat May 19 04:52:24 2007 +0200 @@ -499,7 +499,7 @@ subsection {* Uniform Continuity *} lemma isUCont_isCont: "isUCont f ==> isCont f x" -by (simp add: isUCont_def isCont_def LIM_def, meson) +by (simp add: isUCont_def isCont_def LIM_def, force) subsection {* Relation of LIM and LIMSEQ *}