| author | wenzelm |
| Tue, 28 Aug 2012 18:57:32 +0200 | |
| changeset 48985 | 5386df44a037 |
| parent 16417 | doc-src/TutorialI/Misc/fakenat.thy@9bc16273c2d4 |
| 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 |
(*>*) |