\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}%