
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 *}




