| changeset 37767 | a2b7a20d6ea3 |
| parent 36665 | 5d37a96de20c |
| child 41550 | efa734d9b221 |
--- a/src/HOL/Lim.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/Lim.thy Mon Jul 12 10:48:37 2010 +0200 @@ -23,7 +23,7 @@ definition isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where - [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)" + "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)" subsection {* Limits of Functions *}