NEWS
 changeset 15319 b8da286bb9ad parent 15287 55b7f7920622 child 15350 53d2927d9680
equal 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`