doc-src/TutorialI/Misc/document/fakenat.tex
author nipkow
Wed, 19 Apr 2000 12:59:38 +0200
changeset 8749 2665170f104a
child 9145 9f7b8de5bfaf
permissions -rw-r--r--
Adding generated files

\begin{isabelle}%
%
\begin{isamarkuptext}%
\noindent
The type \isaindexbold{nat} of natural numbers is predefined and
behaves like%
\end{isamarkuptext}%
\isacommand{datatype}~nat~=~{"}0{"}~|~Suc~nat\end{isabelle}%