doc-src/TutorialI/Misc/fakenat.thy
author wenzelm
Wed, 31 May 2000 14:14:45 +0200
changeset 9005 67fb61748d35
parent 8745 13b32661dde4
child 9494 44fefb6e9994
permissions -rw-r--r--
removed 'transfer' att;

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

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

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