--- a/doc-src/TutorialI/Misc/document/Tree2.tex Wed Oct 11 09:09:06 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree2.tex Wed Oct 11 10:44:42 2000 +0200
@@ -9,11 +9,11 @@
quadratic. A linear time version of \isa{flatten} again reqires an extra
argument, the accumulator:%
\end{isamarkuptext}%
-\isacommand{consts}\ flatten\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list{\isachardoublequote}%
+\isacommand{consts}\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list{\isachardoublequote}%
\begin{isamarkuptext}%
-\noindent Define \isa{flatten\isadigit{2}} and prove%
+\noindent Define \isa{flatten{\isadigit{2}}} and prove%
\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}flatten\isadigit{2}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabellebody}%
+\isacommand{lemma}\ {\isachardoublequote}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"