doc-src/TutorialI/Misc/document/Tree2.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/document/Tree2.tex	Wed Aug 02 11:30:38 2000 +0200
@@ -0,0 +1,18 @@
+\begin{isabelle}%
+%
+\begin{isamarkuptext}%
+\noindent In Exercise~\ref{ex:Tree} we defined a function
+\isa{flatten} from trees to lists. The straightforward version of
+\isa{flatten} is based on \isa{\at} and is thus, like \isa{rev}, quadratic.
+A linear time version of \isa{flatten} again reqires an extra
+argument, the accumulator:%
+\end{isamarkuptext}%
+\isacommand{consts}~flatten2~::~{"}'a~tree~=>~'a~list~=>~'a~list{"}%
+\begin{isamarkuptext}%
+\noindent Define \isa{flatten2} and prove%
+\end{isamarkuptext}%
+\isacommand{lemma}~{"}flatten2~t~[]~=~flatten~t{"}\end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: