equal
deleted
inserted
replaced
167 {)\([^\.]*\)\.\. -> {\1<\.\.} |
167 {)\([^\.]*\)\.\. -> {\1<\.\.} |
168 \.\.\([^(}]*\)(} -> \.\.<\1} |
168 \.\.\([^(}]*\)(} -> \.\.<\1} |
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: The syntax for 'setsum', summation over finite sets, has changed: |
|
173 |
|
174 The syntax for 'setsum (%x. e) A' used to be '\<Sum>x:A. e' |
|
175 and is now either 'SUM x:A. e' or '\<Sum>x\<in>A. e'. |
|
176 |
|
177 There is new syntax for summation over finite sets: |
173 |
178 |
174 '\<Sum>x | P. e' is the same as 'setsum (%x. e) {x. P}' |
179 '\<Sum>x | P. e' is the same as 'setsum (%x. e) {x. P}' |
175 '\<Sum>x=a..b. e' is the same as 'setsum (%x. e) {a..b}' |
180 '\<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}' |
181 '\<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}' |
182 '\<Sum>x<k. e' is the same as 'setsum (%x. e) {..<k}' |