now setsum f A = 0 unless A is finite

--- a/src/HOL/Finite.thy	Tue Jun 20 11:41:07 2000 +0200
+++ b/src/HOL/Finite.thy	Tue Jun 20 11:41:25 2000 +0200
@@ -59,7 +59,7 @@
   "fold f e A == @x. (A,x) : foldSet f e"
 
    setsum :: "('a => 'b) => 'a set => ('b::plus_ac0)"
-  "setsum f == fold (op+ o f) 0"
+  "setsum f A == if finite A then fold (op+ o f) 0 A else 0"
 
 locale LC =
   fixes