# HG changeset patch
# User nipkow
# Date 1101197315 -3600
# Node ID 173669c88fd2fce49824465eb8daa42370c74739
# Parent  56c830f91b3885423173bc4e6d98b81e36b6a0c4
generalized lemma

diff -r 56c830f91b38 -r 173669c88fd2 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Nov 23 08:58:32 2004 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Nov 23 09:08:35 2004 +0100
@@ -1025,14 +1025,17 @@
 
 lemma setsum_mult: 
   fixes f :: "'a => ('b::semiring_0_cancel)"
-  assumes fin: "finite A" 
   shows "r * setsum f A = setsum (%n. r * f n) A"
-using fin 
-proof (induct) 
-  case empty thus ?case by simp
+proof (cases "finite A")
+  case True
+  thus ?thesis
+  proof (induct)
+    case empty thus ?case by simp
+  next
+    case (insert A x) thus ?case by (simp add: right_distrib)
+  qed
 next
-  case (insert A x)
-  thus ?case by (simp add: right_distrib) 
+  case False thus ?thesis by (simp add: setsum_def)
 qed
 
 lemma setsum_abs: