diff -r 3ed58bbcf4bd -r 332347b9b942 doc-src/TutorialI/Advanced/advanced.tex --- a/doc-src/TutorialI/Advanced/advanced.tex Mon Jul 16 13:14:19 2001 +0200 +++ b/doc-src/TutorialI/Advanced/advanced.tex Tue Jul 17 13:46:21 2001 +0200 @@ -10,7 +10,7 @@ \input{Advanced/document/simp.tex} \section{Advanced Forms of Recursion} -\index{*recdef|(} +\index{recdef@\isacommand {recdef} (command)|(} The purpose of this section is to introduce advanced forms of \isacommand{recdef}: how to establish termination by means other than measure @@ -41,7 +41,7 @@ \index{partial function} \input{Advanced/document/Partial.tex} -\index{*recdef|)} +\index{recdef@\isacommand {recdef} (command)|)} \section{Advanced Induction Techniques} \label{sec:advanced-ind}