diff -r eacce1cd716a -r 05fc32a23b8b doc-src/TutorialI/Misc/document/fakenat.tex --- a/doc-src/TutorialI/Misc/document/fakenat.tex Tue Aug 16 13:42:21 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/fakenat.tex Tue Aug 16 13:42:23 2005 +0200 @@ -1,16 +1,40 @@ % \begin{isabellebody}% \def\isabellecontext{fakenat}% -\isamarkupfalse% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isamarkuptrue% % \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}\ nat\ {\isacharequal}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ nat\isamarkupfalse% \isamarkupfalse% +\isacommand{datatype}\ nat\ {\isacharequal}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ nat% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory \end{isabellebody}% %%% Local Variables: %%% mode: latex