doc-src/TutorialI/Misc/fakenat.thy
author wenzelm
Mon, 08 May 2000 11:13:28 +0200
changeset 8828 5be2d1745c61
parent 8745 13b32661dde4
child 9494 44fefb6e9994
permissions -rw-r--r--
improved indexing;

(*<*)
theory fakenat = Main:;
(*>*)

text{*\noindent
The type \isaindexbold{nat} of natural numbers is predefined and
behaves like
*}

datatype nat = "0" | Suc nat
(*<*)
end
(*>*)