--- a/src/HOL/Transcendental.thy Fri May 30 12:54:42 2014 +0200
+++ b/src/HOL/Transcendental.thy Fri May 30 14:55:10 2014 +0200
@@ -76,10 +76,7 @@
lemma lemma_realpow_rev_sumr:
"(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) =
(\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
- apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"])
- apply (auto simp: image_iff Bex_def intro!: inj_onI)
- apply arith
- done
+ by (subst nat_diff_setsum_reindex[symmetric]) simp
lemma power_diff_1_eq:
fixes x :: "'a::{comm_ring,monoid_mult}"