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

--- a/doc-src/TutorialI/Misc/document/Tree2.tex	Sun Nov 07 23:32:26 2010 +0100
+++ b/doc-src/TutorialI/Misc/document/Tree2.tex	Mon Nov 08 00:00:47 2010 +0100
@@ -18,12 +18,12 @@
 \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{{\isacharat}} and is thus, like \isa{rev},
+\isa{flatten} is based on \isa{{\isaliteral{40}{\isacharat}}} and is thus, like \isa{rev},
 quadratic. A linear time version of \isa{flatten} again reqires an extra
 argument, the accumulator. Define%
 \end{isamarkuptext}%
 \isamarkuptrue%
-flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}%
+flatten{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}%
 \begin{isamarkuptext}%
 \noindent and prove%
 \end{isamarkuptext}%
@@ -42,7 +42,7 @@
 %
 \endisadelimproof
 \isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequoteclose}%
+\ {\isaliteral{22}{\isachardoublequoteopen}}flatten{\isadigit{2}}\ t\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ flatten\ t{\isaliteral{22}{\isachardoublequoteclose}}%
 \isadelimproof
 %
 \endisadelimproof