1.1 --- a/doc-src/TutorialI/appendix.tex	Wed Oct 18 12:30:59 2000 +0200
     1.2 +++ b/doc-src/TutorialI/appendix.tex	Wed Oct 18 17:19:18 2000 +0200
     1.3 @@ -64,25 +64,26 @@
     1.4  \indexboldpos{\isasymtimes}{$IsaFun}&
     1.5  \ttindexboldpos{*}{$HOL2arithfun} &
     1.6  \verb$\<times>$\\
     1.7 -\indexboldpos{\isasymin}{$HOL3Set}&
     1.8 -\ttindexboldpos{:}{$HOL3Set} &
     1.9 +\indexboldpos{\isasymin}{$HOL3Set0a}&
    1.10 +\ttindexboldpos{:}{$HOL3Set0b} &
    1.11  \verb$\<in>$\\
    1.12 -? & %\indexboldpos{\isasymnotin}{$HOL3Set} fails for some strange reason
    1.13 -\verb$~:$\index{$HOL3Set@\verb$~:$|bold} &
    1.14 +\isasymnotin\index{$HOL3Set0c@\isasymnotin|bold} &
    1.15 +\verb$~:$\index{$HOL3Set0d@\verb$~:$|bold} &
    1.16  \verb$\<notin>$\\
    1.17 -\indexboldpos{\isasymsubseteq}{$HOL3Set}&
    1.18 -\verb$<=$ &
    1.19 -\verb$\<subseteq>$\\
    1.20 -\indexboldpos{\isasymunion}{$HOL3Set}&
    1.21 +\indexboldpos{\isasymsubseteq}{$HOL3Set0e}&
    1.22 +\verb$<=$ & \verb$\<subseteq>$\\
    1.23 +\indexboldpos{\isasymsubset}{$HOL3Set0f}&
    1.24 +\verb$<$ & \verb$\<subset>$\\
    1.25 +\indexboldpos{\isasymunion}{$HOL3Set1}&
    1.26  \ttindexbold{Un} &
    1.27  \verb$\<union>$\\
    1.28 -\indexboldpos{\isasyminter}{$HOL3Set}&
    1.29 +\indexboldpos{\isasyminter}{$HOL3Set1}&
    1.30  \ttindexbold{Int} &
    1.31  \verb$\<inter>$\\
    1.32 -\indexboldpos{\isasymUnion}{$HOL3Set}&
    1.33 +\indexboldpos{\isasymUnion}{$HOL3Set2}&
    1.34  \ttindexbold{UN}, \ttindexbold{Union} &
    1.35  \verb$\<Union>$\\
    1.36 -\indexboldpos{\isasymInter}{$HOL3Set}&
    1.37 +\indexboldpos{\isasymInter}{$HOL3Set2}&
    1.38  \ttindexbold{INT}, \ttindexbold{Inter} &
    1.39  \verb$\<Inter>$\\
    1.40  \hline