--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Mar 18 14:32:23 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Mar 18 15:53:48 2014 +0100
@@ -23,7 +23,7 @@
lemma setsum_mult_product:
"setsum h {..<A * B :: nat} = (\<Sum>i\<in>{..<A}. \<Sum>j\<in>{..<B}. h (j + i * B))"
- unfolding sumr_group[of h B A, unfolded atLeast0LessThan, symmetric]
+ unfolding setsum_nat_group[of h B A, unfolded atLeast0LessThan, symmetric]
proof (rule setsum_cong, simp, rule setsum_reindex_cong)
fix i
show "inj_on (\<lambda>j. j + i * B) {..<B}" by (auto intro!: inj_onI)