| changeset 9087 | 12db178a78df |
| parent 8962 | 633e1682455c |
| child 11092 | 69c1abb9a129 |
--- 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