diff -r d40cc6e7bfd8 -r aea72a834c85 doc-src/TutorialI/Misc/appendix.thy
--- 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"} \\