| author | hoelzl |
| Tue, 29 Mar 2011 14:27:42 +0200 | |
| changeset 42148 | d596e7bb251f |
| parent 16417 | 9bc16273c2d4 |
| 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 |
(*>*) |