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