| changeset 44278 | 1220ecb81e8f |
| parent 43887 | 442aceb54969 |
| child 44344 | 49be3e7d4762 |
--- a/src/HOL/RealDef.thy Thu Aug 18 13:25:17 2011 +0200 +++ b/src/HOL/RealDef.thy Thu Aug 18 13:55:26 2011 +0200 @@ -121,7 +121,7 @@ subsection {* Cauchy sequences *} definition - cauchy :: "(nat \<Rightarrow> rat) set" + cauchy :: "(nat \<Rightarrow> rat) \<Rightarrow> bool" where "cauchy X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r)"