src/HOL/Finite_Set.thy
changeset 22616 4747e87ac5c4
parent 22473 753123c89d72
child 22917 3c56b12fd946
     1.1 --- a/src/HOL/Finite_Set.thy	Mon Apr 09 04:51:28 2007 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Mon Apr 09 21:28:24 2007 +0200
     1.3 @@ -1258,7 +1258,7 @@
     1.4  qed
     1.5  
     1.6  lemma setsum_product:
     1.7 -  fixes f :: "nat => ('a::semiring_0_cancel)"
     1.8 +  fixes f :: "'a => ('b::semiring_0_cancel)"
     1.9    shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
    1.10    by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
    1.11