# HG changeset patch
# User paulson
# Date 961494085 -7200
# Node ID 12db178a78df739d937429922704df25127b8646
# Parent  e4592e43e703c9dfca71ab7ca96395972ccb36c3
now setsum f A = 0 unless A is finite

diff -r e4592e43e703 -r 12db178a78df src/HOL/Finite.thy
--- 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