diff -r 697dcaaf478f -r 0fba0357c04c doc-src/TutorialI/Recdef/document/examples.tex
--- a/doc-src/TutorialI/Recdef/document/examples.tex	Wed Aug 08 14:33:10 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/examples.tex	Wed Aug 08 14:50:28 2001 +0200
@@ -8,7 +8,7 @@
 \isacommand{consts}\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
 \isacommand{recdef}\ fib\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ {\isachardoublequote}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline
-\ \ {\isachardoublequote}fib\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}fib\ {\isadigit{1}}{\isacharprime}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline
 \ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent