src/HOL/Series.thy
changeset 53602 0ae3db699a3e
parent 51528 66c3a7589de7
child 54230 b1d955791529
     1.1 --- a/src/HOL/Series.thy	Thu Sep 12 18:09:56 2013 -0700
     1.2 +++ b/src/HOL/Series.thy	Fri Sep 13 07:59:50 2013 +0200
     1.3 @@ -446,7 +446,7 @@
     1.4  lemma sumr_pos_lt_pair:
     1.5    fixes f :: "nat \<Rightarrow> real"
     1.6    shows "\<lbrakk>summable f;
     1.7 -        \<forall>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
     1.8 +        \<And>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
     1.9        \<Longrightarrow> setsum f {0..<k} < suminf f"
    1.10  unfolding One_nat_def
    1.11  apply (subst suminf_split_initial_segment [where k="k"])