diff -r ca8cd110f769 -r 2d6782e71702 doc-src/TutorialI/Recdef/document/termination.tex
--- a/doc-src/TutorialI/Recdef/document/termination.tex	Tue May 07 14:28:34 2002 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Tue May 07 15:03:50 2002 +0200
@@ -45,7 +45,7 @@
 proved). Because \isacommand{recdef}'s termination prover involves
 simplification, we include in our second attempt a hint: the
 \attrdx{recdef_simp} attribute says to use \isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} as a
-simplification rule.%
+simplification rule.\cmmdx{hints}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%