changeset 48985 | 5386df44a037 |
parent 16417 | 9bc16273c2d4 |
child 56260 | 3d79c132e657 |
48984:f51d4a302962 | 48985:5386df44a037 |
---|---|
1 (*<*) |
|
2 theory fakenat imports Main begin; |
|
3 (*>*) |
|
4 |
|
5 text{*\noindent |
|
6 The type \tydx{nat} of natural |
|
7 numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}. It behaves as if it were declared like this: |
|
8 *} |
|
9 |
|
10 datatype nat = 0 | Suc nat |
|
11 (*<*) |
|
12 end |
|
13 (*>*) |