diff -r e0428c2778f1 -r 028f54cd2cc9 doc-src/TutorialI/appendix.tex
--- a/doc-src/TutorialI/appendix.tex	Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/appendix.tex	Wed Oct 18 17:19:18 2000 +0200
@@ -64,25 +64,26 @@
 \indexboldpos{\isasymtimes}{$IsaFun}&
 \ttindexboldpos{*}{$HOL2arithfun} &
 \verb$\<times>$\\
-\indexboldpos{\isasymin}{$HOL3Set}&
-\ttindexboldpos{:}{$HOL3Set} &
+\indexboldpos{\isasymin}{$HOL3Set0a}&
+\ttindexboldpos{:}{$HOL3Set0b} &
 \verb$\<in>$\\
-? & %\indexboldpos{\isasymnotin}{$HOL3Set} fails for some strange reason
-\verb$~:$\index{$HOL3Set@\verb$~:$|bold} &
+\isasymnotin\index{$HOL3Set0c@\isasymnotin|bold} &
+\verb$~:$\index{$HOL3Set0d@\verb$~:$|bold} &
 \verb$\<notin>$\\
-\indexboldpos{\isasymsubseteq}{$HOL3Set}&
-\verb$<=$ &
-\verb$\<subseteq>$\\
-\indexboldpos{\isasymunion}{$HOL3Set}&
+\indexboldpos{\isasymsubseteq}{$HOL3Set0e}&
+\verb$<=$ & \verb$\<subseteq>$\\
+\indexboldpos{\isasymsubset}{$HOL3Set0f}&
+\verb$<$ & \verb$\<subset>$\\
+\indexboldpos{\isasymunion}{$HOL3Set1}&
 \ttindexbold{Un} &
 \verb$\<union>$\\
-\indexboldpos{\isasyminter}{$HOL3Set}&
+\indexboldpos{\isasyminter}{$HOL3Set1}&
 \ttindexbold{Int} &
 \verb$\<inter>$\\
-\indexboldpos{\isasymUnion}{$HOL3Set}&
+\indexboldpos{\isasymUnion}{$HOL3Set2}&
 \ttindexbold{UN}, \ttindexbold{Union} &
 \verb$\<Union>$\\
-\indexboldpos{\isasymInter}{$HOL3Set}&
+\indexboldpos{\isasymInter}{$HOL3Set2}&
 \ttindexbold{INT}, \ttindexbold{Inter} &
 \verb$\<Inter>$\\
 \hline