diff -r a5f53d9d2b60 -r f8537d69f514 doc-src/TutorialI/Misc/document/Plus.tex
--- a/doc-src/TutorialI/Misc/document/Plus.tex	Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/document/Plus.tex	Thu May 29 22:45:33 2008 +0200
@@ -19,11 +19,9 @@
 \noindent Define the following addition function%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
 \isacommand{primrec}\isamarkupfalse%
-\isanewline
-{\isachardoublequoteopen}add\ m\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
+\ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}add\ m\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\ {\isacharbar}\isanewline
 {\isachardoublequoteopen}add\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ add\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent and prove%