| changeset 23012 | 496b42cf588d |
| parent 22641 | a5dc96fad632 |
| child 23040 | d329182b5966 |
--- 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 *}