diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Misc/document/natsum.tex
--- 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