now setsum f A = 0 unless A is finite
authorpaulson
Tue Jun 20 11:41:25 2000 +0200 (2000-06-20)
changeset 908712db178a78df
parent 9086 e4592e43e703
child 9088 453996655ac2
now setsum f A = 0 unless A is finite
src/HOL/Finite.thy
     1.1 --- a/src/HOL/Finite.thy	Tue Jun 20 11:41:07 2000 +0200
     1.2 +++ b/src/HOL/Finite.thy	Tue Jun 20 11:41:25 2000 +0200
     1.3 @@ -59,7 +59,7 @@
     1.4    "fold f e A == @x. (A,x) : foldSet f e"
     1.5  
     1.6     setsum :: "('a => 'b) => 'a set => ('b::plus_ac0)"
     1.7 -  "setsum f == fold (op+ o f) 0"
     1.8 +  "setsum f A == if finite A then fold (op+ o f) 0 A else 0"
     1.9  
    1.10  locale LC =
    1.11    fixes