diff -r 885a40edcdba -r 0c3891c3528f doc-src/TutorialI/appendix.tex
--- a/doc-src/TutorialI/appendix.tex	Thu Dec 02 12:28:09 2004 +0100
+++ b/doc-src/TutorialI/appendix.tex	Thu Dec 02 14:47:07 2004 +0100
@@ -62,7 +62,7 @@
 \ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} &
 \verb$\<exists>!$\\
 \indexboldpos{\isasymepsilon}{$HOL0ExSome} &
-\ttindexbold{SOME}, \texttt{\at}\index{$HOL2list@\texttt{\at}} &
+\ttindexbold{SOME}, \isa{\at}\index{$HOL2list@\isa{\at}} &
 \verb$\<epsilon>$\\
 \indexboldpos{\isasymcirc}{$HOL1} &
 \ttindexbold{o} &
@@ -71,7 +71,7 @@
 \ttindexbold{abs}&
 \verb$\<bar> \<bar>$\\
 \indexboldpos{\isasymle}{$HOL2arithrel}&
-\ttindexboldpos{<=}{$HOL2arithrel}&
+\isadxboldpos{<=}{$HOL2arithrel}&
 \verb$\<le>$\\
 \indexboldpos{\isasymtimes}{$Isatype}&
 \ttindexboldpos{*}{$HOL2arithfun} &