changeset 47217 | 501b9bbd0d6e |
parent 37765 | 26bdfb7b680b |
child 51525 | d3d170a2887f |
--- a/src/HOL/NSA/HSeries.thy Fri Mar 30 10:41:27 2012 +0200 +++ b/src/HOL/NSA/HSeries.thy Fri Mar 30 11:16:35 2012 +0200 @@ -114,7 +114,7 @@ lemma sumhr_minus_one_realpow_zero [simp]: "!!N. sumhr(0, N + N, %i. (-1) ^ (i+1)) = 0" unfolding sumhr_app -by transfer (simp del: power_Suc add: nat_mult_2 [symmetric]) +by transfer (simp del: power_Suc add: mult_2 [symmetric]) lemma sumhr_interval_const: "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na