--- 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.