--- a/doc-src/TutorialI/Recdef/document/termination.tex Wed Dec 13 09:32:55 2000 +0100
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Wed Dec 13 09:39:53 2000 +0100
@@ -39,7 +39,7 @@
\noindent
Because \isacommand{recdef}'s termination prover involves simplification,
we include with our second attempt the hint to use \isa{termi{\isacharunderscore}lem} as
-a simplification rule:%
+a simplification rule:\indexbold{*recdef_simp}%
\end{isamarkuptext}%
\isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline