--- a/doc-src/TutorialI/Recdef/document/Nested0.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Thu Aug 09 18:12:15 2001 +0200
@@ -3,6 +3,7 @@
\def\isabellecontext{Nested{\isadigit{0}}}%
%
\begin{isamarkuptext}%
+\index{datatypes!nested}%
In \S\ref{sec:nested-datatype} we defined the datatype of terms%
\end{isamarkuptext}%
\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}a\ {\isacharbar}\ App\ {\isacharprime}b\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isachardoublequote}%