--- a/doc-src/TutorialI/Misc/document/natsum.tex Wed Oct 11 09:09:06 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Wed Oct 11 10:44:42 2000 +0200
@@ -6,12 +6,12 @@
\noindent
In particular, there are \isa{case}-expressions, for example
\begin{isabelle}%
-\ \ \ \ \ case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m%
+\ \ \ \ \ case\ n\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m%
\end{isabelle}
primitive recursion, for example%
\end{isamarkuptext}%
\isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
-\isacommand{primrec}\ {\isachardoublequote}sum\ \isadigit{0}\ {\isacharequal}\ \isadigit{0}{\isachardoublequote}\isanewline
+\isacommand{primrec}\ {\isachardoublequote}sum\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline
\ \ \ \ \ \ \ \ {\isachardoublequote}sum\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharplus}\ sum\ n{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent