--- a/doc-src/TutorialI/Misc/document/natsum.tex Mon Mar 19 13:28:06 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Mon Mar 19 17:25:42 2001 +0100
@@ -61,7 +61,7 @@
\end{warn}
Simple arithmetic goals are proved automatically by both \isa{auto} and the
-simplification methods introduced in \S\ref{sec:Simplification}. For
+simplification method introduced in \S\ref{sec:Simplification}. For
example,%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%