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