# HG changeset patch
# User huffman
# Date 1176146904 -7200
# Node ID 4747e87ac5c4fd3ae6153d9a6b1d71c9f81c864f
# Parent  d650e51b5970e7ccb3f7b48cb3e9ac41946fff25
generalized type of lemma setsum_product

diff -r d650e51b5970 -r 4747e87ac5c4 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Apr 09 04:51:28 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Apr 09 21:28:24 2007 +0200
@@ -1258,7 +1258,7 @@
 qed
 
 lemma setsum_product:
-  fixes f :: "nat => ('a::semiring_0_cancel)"
+  fixes f :: "'a => ('b::semiring_0_cancel)"
   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)