
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Misc/natsum.thy
--- a/doc-src/TutorialI/Misc/natsum.thy	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy	Tue Sep 05 09:03:17 2000 +0200
@@ -3,9 +3,7 @@
 (*>*)
 text{*\noindent
 In particular, there are @{text"case"}-expressions, for example
-\begin{quote}
 @{term[display]"case n of 0 => 0 | Suc m => m"}
-\end{quote}
 primitive recursion, for example
 *}
 




