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