--- a/doc-src/TutorialI/Misc/document/natsum.tex Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Tue Sep 05 09:03:17 2000 +0200
@@ -4,13 +4,11 @@
\begin{isamarkuptext}%
\noindent
In particular, there are \isa{case}-expressions, for example
-\begin{quote}
-
+%
\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}%
-\end{quote}
primitive recursion, for example%
\end{isamarkuptext}%
\isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline