doc-src/TutorialI/Misc/natsum.thy
changeset 9834 109b11c4e77e
parent 9792 bbefb6ce5cb2
child 10171 59d6633835fa
--- 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
 *}