equal
deleted
inserted
replaced
61 setsum :: "('a => 'b) => 'a set => 'b::plus_ac0" |
61 setsum :: "('a => 'b) => 'a set => 'b::plus_ac0" |
62 "setsum f A == if finite A then fold (op+ o f) 0 A else 0" |
62 "setsum f A == if finite A then fold (op+ o f) 0 A else 0" |
63 |
63 |
64 syntax |
64 syntax |
65 "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\\<Sum>_:_. _" [0, 51, 10] 10) |
65 "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\\<Sum>_:_. _" [0, 51, 10] 10) |
66 syntax (symbols) |
66 syntax (xsymbols) |
67 "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\\<Sum>_\\<in>_. _" [0, 51, 10] 10) |
67 "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\\<Sum>_\\<in>_. _" [0, 51, 10] 10) |
68 translations |
68 translations |
69 "\\<Sum>i:A. b" == "setsum (%i. b) A" (* Beware of argument permutation! *) |
69 "\\<Sum>i:A. b" == "setsum (%i. b) A" (* Beware of argument permutation! *) |
70 |
70 |
71 |
71 |