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 