doc-src/TutorialI/Advanced/advanced.tex
changeset 11428 332347b9b942
parent 11216 279004936bb0
child 11494 23a118849801
--- 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}