doc-src/TutorialI/appendix.tex

--- a/doc-src/TutorialI/appendix.tex	Tue Feb 20 10:18:26 2001 +0100
+++ b/doc-src/TutorialI/appendix.tex	Tue Feb 20 10:37:12 2001 +0100
@@ -53,7 +53,7 @@
 \ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} &
 \verb$\<exists>!$\\
 \indexboldpos{\isasymepsilon}{$HOL0ExSome} &
-\ttindexbold{SOME} &
+\ttindexbold{SOME}, \texttt{\at}\index{$HOL2list@\texttt{\at}} &
 \verb$\<epsilon>$\\
 \indexboldpos{\isasymcirc}{$HOL1} &
 \ttindexbold{o} &