diff -r f8353c722d4e -r a2bff98d6e5d doc-src/TutorialI/Recdef/document/Nested1.tex
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex	Tue May 01 17:16:32 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex	Tue May 01 22:26:55 2001 +0200
@@ -4,7 +4,7 @@
 %
 \begin{isamarkuptext}%
 \noindent
-Although the definition of \isa{trev} is quite natural, we will have
+Although the definition of \isa{trev} below is quite natural, we will have
 to overcome a minor difficulty in convincing Isabelle of its termination.
 It is precisely this difficulty that is the \textit{raison d'\^etre} of
 this subsection.