diff -r f3ff2549cdc8 -r 23a118849801 doc-src/TutorialI/Recdef/document/Nested0.tex
--- 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}%