| changeset 58889 | 5b7a9633cfa8 |
| parent 58729 | e8ecc79aee43 |
| child 59000 | 6eb0725503fc |
| 58888:9537bf1c4853 | 58889:5b7a9633cfa8 |
|---|---|
5 Converted to Isar and polished by lcp |
5 Converted to Isar and polished by lcp |
6 Converted to setsum and polished yet more by TNN |
6 Converted to setsum and polished yet more by TNN |
7 Additional contributions by Jeremy Avigad |
7 Additional contributions by Jeremy Avigad |
8 *) |
8 *) |
9 |
9 |
10 header {* Infinite Series *} |
10 section {* Infinite Series *} |
11 |
11 |
12 theory Series |
12 theory Series |
13 imports Limits |
13 imports Limits |
14 begin |
14 begin |
15 |
15 |