--- a/doc-src/TutorialI/Misc/document/Plus.tex Sat Mar 11 17:24:37 2006 +0100
+++ b/doc-src/TutorialI/Misc/document/Plus.tex Sat Mar 11 17:30:35 2006 +0100
@@ -20,11 +20,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\isamarkupfalse%
-\ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
+\ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
\isanewline
-{\isachardoublequoteopen}plus\ m\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}plus\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ plus\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n{\isachardoublequoteclose}%
+{\isachardoublequoteopen}add\ m\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
+{\isachardoublequoteopen}add\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ add\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent and prove%
\end{isamarkuptext}%
@@ -43,7 +43,7 @@
%
\endisadelimproof
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}plus\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequoteclose}%
+\ {\isachardoublequoteopen}add\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequoteclose}%
\isadelimproof
%
\endisadelimproof