doc-src/TutorialI/Misc/natsum.thy

--- a/doc-src/TutorialI/Misc/natsum.thy	Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy	Sun Aug 06 15:26:53 2000 +0200
@@ -3,11 +3,9 @@
 (*>*)
 text{*\noindent
 In particular, there are \isa{case}-expressions, for example
-*}
-
-(*<*)term(*>*) "case n of 0 \\<Rightarrow> 0 | Suc m \\<Rightarrow> m";
-
-text{*\noindent
+\begin{quote}
+@{term[display]"case n of 0 => 0 | Suc m => m"}
+\end{quote}
 primitive recursion, for example
 *}