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