diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Recdef/Nested1.thy
--- a/doc-src/TutorialI/Recdef/Nested1.thy	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy	Tue Sep 05 09:03:17 2000 +0200
@@ -22,9 +22,7 @@
 Remember that function @{term"size"} is defined for each \isacommand{datatype}.
 However, the definition does not succeed. Isabelle complains about an
 unproved termination condition
-\begin{quote}
 @{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
-\end{quote}
 where @{term"set"} returns the set of elements of a list (no special
 knowledge of sets is required in the following) and @{text"term_list_size ::
 term list \<Rightarrow> nat"} is an auxiliary function automatically defined by Isabelle