diff -r b44ad7e4c4d2 -r 279004936bb0 doc-src/TutorialI/Misc/document/natsum.tex --- 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}%