
diff -r a39e5d43de55 -r bbefb6ce5cb2 doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Fri Sep 01 19:09:44 2000 +0200
@@ -7,7 +7,7 @@
 \begin{quote}
 
 \begin{isabelle}%
-case\ \mbox{n}\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ \mbox{m}\ {\isasymRightarrow}\ \mbox{m}
+case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m
 \end{isabelle}%
 
 \end{quote}




