--- 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"