--- a/doc-src/TutorialI/Advanced/document/WFrec.tex Tue Jul 17 13:46:21 2001 +0200
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Tue Jul 17 15:07:36 2001 +0200
@@ -101,8 +101,8 @@
\begin{isamarkuptext}%
\noindent
-Armed with this lemma, we can append a crucial hint to our definition:
-\indexbold{*recdef_wf}%
+Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a
+crucial hint to our definition:%
\end{isamarkuptext}%
{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}%
\begin{isamarkuptext}%