src/HOL/Hyperreal/SEQ.thy
changeset 28562 4e74209f113e
parent 27681 8cedebf55539
child 28823 dcbef866c9e2
     1.1 --- a/src/HOL/Hyperreal/SEQ.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -15,13 +15,13 @@
     1.4  definition
     1.5    Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where
     1.6      --{*Standard definition of sequence converging to zero*}
     1.7 -  [code func del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
     1.8 +  [code del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
     1.9  
    1.10  definition
    1.11    LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
    1.12      ("((_)/ ----> (_))" [60, 60] 60) where
    1.13      --{*Standard definition of convergence of sequence*}
    1.14 -  [code func del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
    1.15 +  [code del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
    1.16  
    1.17  definition
    1.18    lim :: "(nat => 'a::real_normed_vector) => 'a" where
    1.19 @@ -36,22 +36,22 @@
    1.20  definition
    1.21    Bseq :: "(nat => 'a::real_normed_vector) => bool" where
    1.22      --{*Standard definition for bounded sequence*}
    1.23 -  [code func del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
    1.24 +  [code del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
    1.25  
    1.26  definition
    1.27    monoseq :: "(nat=>real)=>bool" where
    1.28      --{*Definition for monotonicity*}
    1.29 -  [code func del]: "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
    1.30 +  [code del]: "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
    1.31  
    1.32  definition
    1.33    subseq :: "(nat => nat) => bool" where
    1.34      --{*Definition of subsequence*}
    1.35 -  [code func del]:   "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
    1.36 +  [code del]:   "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
    1.37  
    1.38  definition
    1.39    Cauchy :: "(nat => 'a::real_normed_vector) => bool" where
    1.40      --{*Standard definition of the Cauchy condition*}
    1.41 -  [code func del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
    1.42 +  [code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
    1.43  
    1.44  
    1.45  subsection {* Bounded Sequences *}