| changeset 58889 | 5b7a9633cfa8 |
| parent 58820 | 3ad2759acc52 |
| child 58952 | 5d82cdef6c1b |
| 58888:9537bf1c4853 | 58889:5b7a9633cfa8 |
|---|---|
3 |
3 |
4 Type "nat" is a linear order, and a datatype; arithmetic operators + - |
4 Type "nat" is a linear order, and a datatype; arithmetic operators + - |
5 and * (for div and mod, see theory Divides). |
5 and * (for div and mod, see theory Divides). |
6 *) |
6 *) |
7 |
7 |
8 header {* Natural numbers *} |
8 section {* Natural numbers *} |
9 |
9 |
10 theory Nat |
10 theory Nat |
11 imports Inductive Typedef Fun Fields |
11 imports Inductive Typedef Fun Fields |
12 begin |
12 begin |
13 |
13 |