diff -r 5a4d78204492 -r 7c4ec77a8715 doc-src/TutorialI/Misc/document/natsum.tex --- a/doc-src/TutorialI/Misc/document/natsum.tex Thu Nov 29 13:33:45 2001 +0100 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Thu Nov 29 14:12:42 2001 +0100 @@ -70,7 +70,7 @@ tactics (like \isa{auto}, \isa{simp} and \isa{arith}) but not by others (especially the single step tactics in Chapter~\ref{chap:rules}). If you need the full set of numerals, see~\S\ref{sec:numerals}. - \emph{Novices are advised to stick to \isa{{\isadigit{0}}} and of \isa{Suc}.} + \emph{Novices are advised to stick to \isa{{\isadigit{0}}} and \isa{Suc}.} \end{warn} Both \isa{auto} and \isa{simp}