diff -r 6c45813c2db1 -r d27253c4594f doc-src/TutorialI/Misc/document/appendix.tex
--- a/doc-src/TutorialI/Misc/document/appendix.tex	Mon Oct 08 12:27:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/appendix.tex	Mon Oct 08 12:28:43 2001 +0200
@@ -8,7 +8,7 @@
 \begin{tabular}{lll}
 Constant & Type & Syntax \\
 \hline
-\isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
+\isa{{\isadigit{0}}{\isasymColon}{\isacharprime}a} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
 \isa{{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}plus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
 \isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} &  (infixl 65) \\
 \isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\