doc-src/TutorialI/Recdef/Nested1.thy

--- a/doc-src/TutorialI/Recdef/Nested1.thy	Tue May 01 17:16:32 2001 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy	Tue May 01 22:26:55 2001 +0200
@@ -3,7 +3,7 @@
 (*>*)
 
 text{*\noindent
-Although the definition of @{term trev} is quite natural, we will have
+Although the definition of @{term 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.