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