--- 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} &