--- a/doc-src/TutorialI/Recdef/Nested0.thy Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Recdef/Nested0.thy Wed Mar 07 15:54:11 2001 +0100
@@ -13,7 +13,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 @{term"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}: