62 \ttindexboldpos{<=}{$HOL2arithrel}& |
62 \ttindexboldpos{<=}{$HOL2arithrel}& |
63 \verb$\<le>$\\ |
63 \verb$\<le>$\\ |
64 \indexboldpos{\isasymtimes}{$IsaFun}& |
64 \indexboldpos{\isasymtimes}{$IsaFun}& |
65 \ttindexboldpos{*}{$HOL2arithfun} & |
65 \ttindexboldpos{*}{$HOL2arithfun} & |
66 \verb$\<times>$\\ |
66 \verb$\<times>$\\ |
67 \indexboldpos{\isasymin}{$HOL3Set}& |
67 \indexboldpos{\isasymin}{$HOL3Set0a}& |
68 \ttindexboldpos{:}{$HOL3Set} & |
68 \ttindexboldpos{:}{$HOL3Set0b} & |
69 \verb$\<in>$\\ |
69 \verb$\<in>$\\ |
70 ? & %\indexboldpos{\isasymnotin}{$HOL3Set} fails for some strange reason |
70 \isasymnotin\index{$HOL3Set0c@\isasymnotin|bold} & |
71 \verb$~:$\index{$HOL3Set@\verb$~:$|bold} & |
71 \verb$~:$\index{$HOL3Set0d@\verb$~:$|bold} & |
72 \verb$\<notin>$\\ |
72 \verb$\<notin>$\\ |
73 \indexboldpos{\isasymsubseteq}{$HOL3Set}& |
73 \indexboldpos{\isasymsubseteq}{$HOL3Set0e}& |
74 \verb$<=$ & |
74 \verb$<=$ & \verb$\<subseteq>$\\ |
75 \verb$\<subseteq>$\\ |
75 \indexboldpos{\isasymsubset}{$HOL3Set0f}& |
76 \indexboldpos{\isasymunion}{$HOL3Set}& |
76 \verb$<$ & \verb$\<subset>$\\ |
|
77 \indexboldpos{\isasymunion}{$HOL3Set1}& |
77 \ttindexbold{Un} & |
78 \ttindexbold{Un} & |
78 \verb$\<union>$\\ |
79 \verb$\<union>$\\ |
79 \indexboldpos{\isasyminter}{$HOL3Set}& |
80 \indexboldpos{\isasyminter}{$HOL3Set1}& |
80 \ttindexbold{Int} & |
81 \ttindexbold{Int} & |
81 \verb$\<inter>$\\ |
82 \verb$\<inter>$\\ |
82 \indexboldpos{\isasymUnion}{$HOL3Set}& |
83 \indexboldpos{\isasymUnion}{$HOL3Set2}& |
83 \ttindexbold{UN}, \ttindexbold{Union} & |
84 \ttindexbold{UN}, \ttindexbold{Union} & |
84 \verb$\<Union>$\\ |
85 \verb$\<Union>$\\ |
85 \indexboldpos{\isasymInter}{$HOL3Set}& |
86 \indexboldpos{\isasymInter}{$HOL3Set2}& |
86 \ttindexbold{INT}, \ttindexbold{Inter} & |
87 \ttindexbold{INT}, \ttindexbold{Inter} & |
87 \verb$\<Inter>$\\ |
88 \verb$\<Inter>$\\ |
88 \hline |
89 \hline |
89 \end{tabular} |
90 \end{tabular} |
90 \end{center} |
91 \end{center} |