--- a/doc-src/TutorialI/Misc/appendix.thy Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Misc/appendix.thy Thu Nov 29 21:12:37 2001 +0100
@@ -8,7 +8,8 @@
\begin{tabular}{lll}
Constant & Type & Syntax \\
\hline
-@{term 0} & @{text "'a::zero"} \\
+@{text 0} & @{text "'a::zero"} \\
+@{text 1} & @{text "'a::one"} \\
@{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\