equal
deleted
inserted
replaced
169 |
169 |
170 They are not perfect but work quite well. |
170 They are not perfect but work quite well. |
171 |
171 |
172 * HOL: There is new syntax for summation over finite sets: |
172 * HOL: There is new syntax for summation over finite sets: |
173 |
173 |
174 '\<Sum>x | P. e' is the same as 'setsum (%x. e) {x. P}' |
174 '\<Sum>x | P. e' is the same as 'setsum (%x. e) {x. P}' |
175 '\<Sum>x<k. e' is the same as 'setsum (%x. e) {..<k}' |
175 '\<Sum>x=a..b. e' is the same as 'setsum (%x. e) {a..b}' |
|
176 '\<Sum>x=a..<b. e' is the same as 'setsum (%x. e) {a..<b}' |
|
177 '\<Sum>x<k. e' is the same as 'setsum (%x. e) {..<k}' |
176 |
178 |
177 Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e' |
179 Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e' |
178 now translates into 'setsum' as above. |
180 now translates into 'setsum' as above. |
179 |
181 |
180 |
182 |