src/HOL/Series.thy

--- a/src/HOL/Series.thy	Mon Oct 05 16:41:06 2009 +0100
+++ b/src/HOL/Series.thy	Mon Oct 05 17:27:46 2009 +0100
@@ -32,6 +32,9 @@
   "\<Sum>i. b" == "CONST suminf (%i. b)"
 
 
+lemma [trans]: "f=g ==> g sums z ==> f sums z"
+  by simp
+
 lemma sumr_diff_mult_const:
  "setsum f {0..<n} - (real n*r) = setsum (%i. f i - r) {0..<n::nat}"
 by (simp add: diff_minus setsum_addf real_of_nat_def)