--- 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%