diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Advanced/WFrec.thy
--- a/doc-src/TutorialI/Advanced/WFrec.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Advanced/WFrec.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -79,7 +79,7 @@
 by simp;
 
 text{*\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}
 *}
 (*<*)