--- a/doc-src/TutorialI/Recdef/document/termination.tex Tue Jul 17 13:46:21 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Tue Jul 17 15:07:36 2001 +0200
@@ -38,8 +38,9 @@
\begin{isamarkuptext}%
\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:\indexbold{*recdef_simp}%
+we include in our second attempt a hint: the \attrdx{recdef_simp} attribute
+says to use \isa{termi{\isacharunderscore}lem} as
+a simplification rule.%
\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