doc-src/TutorialI/Misc/document/appendix.tex
changeset 12332 aea72a834c85
parent 11866 fbd097aec213
child 13758 ee898d32de21
--- a/doc-src/TutorialI/Misc/document/appendix.tex	Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/appendix.tex	Thu Nov 29 21:12:37 2001 +0100
@@ -9,7 +9,8 @@
 \begin{tabular}{lll}
 Constant & Type & Syntax \\
 \hline
-\isa{{\isadigit{0}}{\isasymColon}{\isacharprime}a} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
+\isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
+\isa{{\isadigit{1}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}one} \\
 \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} \\