| changeset 14706 | 71590b7733b7 |
| parent 14691 | e1eedc8cad37 |
| child 14981 | e73f8140af78 |
| 14705:14b2c22a7e40 | 14706:71590b7733b7 |
|---|---|
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: David von Oheimb, TU Muenchen |
3 Author: David von Oheimb, TU Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 *) |
5 *) |
6 |
6 |
7 header {* |
7 header {* Natural numbers with infinity *} |
8 \title{Natural numbers with infinity} |
|
9 \author{David von Oheimb} |
|
10 *} |
|
11 |
8 |
12 theory Nat_Infinity = Main: |
9 theory Nat_Infinity = Main: |
13 |
10 |
14 subsection "Definitions" |
11 subsection "Definitions" |
15 |
12 |