equal
deleted
inserted
replaced
218 '\<Sum>x=a..<b. e' is the same as 'setsum (%x. e) {a..<b}' |
218 '\<Sum>x=a..<b. e' is the same as 'setsum (%x. e) {a..<b}' |
219 '\<Sum>x<k. e' is the same as 'setsum (%x. e) {..<k}' |
219 '\<Sum>x<k. e' is the same as 'setsum (%x. e) {..<k}' |
220 |
220 |
221 Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e' |
221 Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e' |
222 now translates into 'setsum' as above. |
222 now translates into 'setsum' as above. |
|
223 |
|
224 * HOL: Finite set induction: In Isar proofs, the insert case is now |
|
225 "case (insert x F)" instead of the old counterintuitive "case (insert F x)". |
223 |
226 |
224 * HOL/Simplifier: |
227 * HOL/Simplifier: |
225 |
228 |
226 - Is now set up to reason about transitivity chains involving "trancl" |
229 - Is now set up to reason about transitivity chains involving "trancl" |
227 (r^+) and "rtrancl" (r^*) by setting up tactics provided by |
230 (r^+) and "rtrancl" (r^*) by setting up tactics provided by |