diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Advanced/document/WFrec.tex
--- 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}%