1.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex	Mon Sep 04 21:20:14 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex	Tue Sep 05 09:03:17 2000 +0200
     1.3 @@ -4,13 +4,11 @@
     1.4  \begin{isamarkuptext}%
     1.5  \noindent
     1.6  In particular, there are \isa{case}-expressions, for example
     1.7 -\begin{quote}
     1.8 -
     1.9 +%
    1.10  \begin{isabelle}%
    1.11 -case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m
    1.12 +\ \ \ \ \ case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m%
    1.13  \end{isabelle}%
    1.14  
    1.15 -\end{quote}
    1.16  primitive recursion, for example%
    1.17  \end{isamarkuptext}%
    1.18  \isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline