--- a/doc-src/TutorialI/Misc/document/Tree.tex Sun Nov 07 23:32:26 2010 +0100
+++ b/doc-src/TutorialI/Misc/document/Tree.tex Mon Nov 08 00:00:47 2010 +0100
@@ -21,7 +21,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\isamarkupfalse%
-\ {\isacharprime}a\ tree\ {\isacharequal}\ Tip\ {\isacharbar}\ Node\ {\isachardoublequoteopen}{\isacharprime}a\ tree{\isachardoublequoteclose}\ {\isacharprime}a\ {\isachardoublequoteopen}{\isacharprime}a\ tree{\isachardoublequoteclose}%
+\ {\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{3D}{\isacharequal}}\ Tip\ {\isaliteral{7C}{\isacharbar}}\ Node\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
\noindent
Define a function \isa{mirror} that mirrors a binary tree
@@ -29,7 +29,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequoteopen}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequoteclose}%
+\ mirror{\isaliteral{5F}{\isacharunderscore}}mirror{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}mirror{\isaliteral{28}{\isacharparenleft}}mirror\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequoteclose}}%
\isadelimproof
%
\endisadelimproof
@@ -50,7 +50,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequoteclose}%
+\ {\isaliteral{22}{\isachardoublequoteopen}}flatten{\isaliteral{28}{\isacharparenleft}}mirror\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rev{\isaliteral{28}{\isacharparenleft}}flatten\ t{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\isadelimproof
%
\endisadelimproof