changeset 41777 | 1f7cbe39d425 |
parent 35762 | af3ff2ba4c54 |
child 65449 | c82e63b11b8b |
41776:3bd83302a3c3 | 41777:1f7cbe39d425 |
---|---|
1 (* Title: ZF/ex/Natsum.thy |
1 (* Title: ZF/ex/NatSum.thy |
2 Author: Tobias Nipkow & Lawrence C Paulson |
2 Author: Tobias Nipkow & Lawrence C Paulson |
3 |
3 |
4 A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n. |
4 A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n. |
5 |
5 |
6 Note: n is a natural number but the sum is an integer, |
6 Note: n is a natural number but the sum is an integer, |