1
(*<*)
2
theory fakenat = Main:;
3
(*>*)
4
5
text{*\noindent
6
The type \isaindexbold{nat} of natural numbers is predefined and
7
behaves like
8
*}
9
10
datatype nat = "0" | Suc nat
11
12
end
13