--- a/doc-src/TutorialI/Advanced/document/WFrec.tex Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Fri Jan 05 18:32:57 2001 +0100
@@ -76,7 +76,7 @@
\isacommand{by}\ simp%
\begin{isamarkuptext}%
\noindent
-and should have appended the following hint to our above definition:
+and should have appended the following hint to our definition above:
\indexbold{*recdef_wf}%
\end{isamarkuptext}%
{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}id{\isacharparenright}\end{isabellebody}%