doc-src/TutorialI/Advanced/WFrec.thy

--- a/doc-src/TutorialI/Advanced/WFrec.thy	Tue Jul 17 13:46:21 2001 +0200
+++ b/doc-src/TutorialI/Advanced/WFrec.thy	Tue Jul 17 15:07:36 2001 +0200
@@ -105,8 +105,8 @@
 
 text{*\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:
 *}
 (*<*)
 consts g :: "nat \<Rightarrow> nat"