--- a/doc-src/TutorialI/Advanced/WFrec.thy Wed Dec 13 09:32:55 2000 +0100
+++ b/doc-src/TutorialI/Advanced/WFrec.thy Wed Dec 13 09:39:53 2000 +0100
@@ -5,7 +5,7 @@
functions. Sometimes this can be quite inconvenient or even
impossible. Fortunately, \isacommand{recdef} supports much more
general definitions. For example, termination of Ackermann's function
-can be shown by means of the lexicographic product @{text"<*lex*>"}:
+can be shown by means of the \rmindex{lexicographic product} @{text"<*lex*>"}:
*}
consts ack :: "nat\<times>nat \<Rightarrow> nat";
@@ -80,6 +80,7 @@
text{*\noindent
and should have appended the following hint to our above definition:
+\indexbold{*recdef_wf}
*}
(*<*)
consts g :: "nat \<Rightarrow> nat"
@@ -87,5 +88,5 @@
"g 0 = 0"
"g (Suc n) = g n"
(*>*)
-(hints recdef_wf add: wf_id)
+(hints recdef_wf: wf_id)
(*<*)end(*>*)