| author | nipkow |
| Tue, 08 Jan 2013 10:34:19 +0100 | |
| changeset 50766 | d5c07ddd929b |
| parent 48985 | 5386df44a037 |
| child 56260 | 3d79c132e657 |
| permissions | -rw-r--r-- |
| 8745 | 1 |
(*<*) |
| 16417 | 2 |
theory fakenat imports Main begin; |
| 8745 | 3 |
(*>*) |
4 |
||
5 |
text{*\noindent
|
|
| 11418 | 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:
|
|
| 8745 | 8 |
*} |
9 |
||
| 9541 | 10 |
datatype nat = 0 | Suc nat |
| 8745 | 11 |
(*<*) |
12 |
end |
|
13 |
(*>*) |