author | wenzelm |
Sat, 11 Aug 2012 18:05:41 +0200 | |
changeset 48771 | 2ea997196d04 |
parent 48519 | 5deda0549f97 |
permissions | -rw-r--r-- |
% \begin{isabellebody}% \def\isabellecontext{fakenat}% % \isadelimtheory % \endisadelimtheory % \isatagtheory % \endisatagtheory {\isafoldtheory}% % \isadelimtheory % \endisadelimtheory % \begin{isamarkuptext}% \noindent The type \tydx{nat} of natural numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}. It behaves as if it were declared like this:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{datatype}\isamarkupfalse% \ nat\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}\ Suc\ nat% \isadelimtheory % \endisadelimtheory % \isatagtheory % \endisatagtheory {\isafoldtheory}% % \isadelimtheory % \endisadelimtheory \end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" %%% End: