diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Misc/case_exprs.thy
--- a/doc-src/TutorialI/Misc/case_exprs.thy	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/case_exprs.thy	Tue Sep 05 09:03:17 2000 +0200
@@ -7,9 +7,7 @@
 text{*\label{sec:case-expressions}
 HOL also features \isaindexbold{case}-expressions for analyzing
 elements of a datatype. For example,
-\begin{quote}
 @{term[display]"case xs of [] => 1 | y#ys => y"}
-\end{quote}
 evaluates to @{term"1"} if @{term"xs"} is @{term"[]"} and to @{term"y"} if 
 @{term"xs"} is @{term"y#ys"}. (Since the result in both branches must be of
 the same type, it follows that @{term"y"} is of type @{typ"nat"} and hence
@@ -34,15 +32,9 @@
 \noindent
 Nested patterns can be simulated by nested @{text"case"}-expressions: instead
 of
-% 
-\begin{quote}
-@{text"case xs of [] => 1 | [x] => x | x#(y#zs) => y"}
-%~~~case~xs~of~[]~{\isasymRightarrow}~1~|~[x]~{\isasymRightarrow}~x~|~x~\#~y~\#~zs~{\isasymRightarrow}~y
-\end{quote}
+@{text[display]"case xs of [] => 1 | [x] => x | x # (y # zs) => y"}
 write
-\begin{quote}
 @{term[display,eta_contract=false,margin=50]"case xs of [] => 1 | x#ys => (case ys of [] => x | y#zs => y)"}
-\end{quote}
 
 Note that @{text"case"}-expressions may need to be enclosed in parentheses to
 indicate their scope