| changeset 28952 | 15a4b2cf8c34 |
| parent 23477 | f4b83f03cac9 |
| child 40077 | c8a9eaaa2f59 |
| 28948:1860f016886d | 28952:15a4b2cf8c34 |
|---|---|
1 (* Title: HOL/ex/NatSum.thy |
1 (* Title: HOL/ex/NatSum.thy |
2 ID: $Id$ |
2 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
|
4 *) |
3 *) |
5 |
4 |
6 header {* Summing natural numbers *} |
5 header {* Summing natural numbers *} |
7 |
6 |
8 theory NatSum imports Main Parity begin |
7 theory NatSum imports Main Parity begin |