
diff -r d666cb0e4cf9 -r c726ecfb22b6 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- 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)




