diff -r 72e429c66608 -r 494f8cd34df7 doc-src/TutorialI/Misc/document/Tree.tex
--- a/doc-src/TutorialI/Misc/document/Tree.tex	Tue Aug 01 18:26:34 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree.tex	Wed Aug 02 11:30:38 2000 +0200
@@ -10,7 +10,13 @@
 and a function \isa{mirror} that mirrors a binary tree
 by swapping subtrees (recursively). Prove%
 \end{isamarkuptext}%
-\isacommand{lemma}~mirror\_mirror:~{"}mirror(mirror~t)~=~t{"}\end{isabelle}%
+\isacommand{lemma}~mirror\_mirror:~{"}mirror(mirror~t)~=~t{"}%
+\begin{isamarkuptext}%
+\noindent
+Define a function \isa{flatten} that flattens a tree into a list
+by traversing it in infix order. Prove%
+\end{isamarkuptext}%
+\isacommand{lemma}~{"}flatten(mirror~t)~=~rev(flatten~t){"}\end{isabelle}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"