--- a/doc-src/TutorialI/Recdef/document/Nested0.tex Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Wed Mar 07 15:54:11 2001 +0100
@@ -12,7 +12,7 @@
of primitive recursive functions leads to overly verbose definitions. Moreover,
if you have worked exercise~\ref{ex:trev-trev} you will have noticed that
you needed to declare essentially the same function as \isa{rev}
-and prove many standard properties of list reverse all over again.
+and prove many standard properties of list reversal all over again.
We will now show you how \isacommand{recdef} can simplify
definitions and proofs about nested recursive datatypes. As an example we
choose exercise~\ref{ex:trev-trev}:%