1
\begin{isabelle}%
2
%
3
\begin{isamarkuptext}%
4
\noindent
5
The type \isaindexbold{nat} of natural numbers is predefined and
6
behaves like%
7
\end{isamarkuptext}%
8
\isacommand{datatype}~nat~=~{"}0{"}~|~Suc~nat\end{isabelle}%