--- a/doc-src/TutorialI/appendix.tex Sat Jan 06 11:27:09 2001 +0100
+++ b/doc-src/TutorialI/appendix.tex Sat Jan 06 12:39:05 2001 +0100
@@ -89,6 +89,12 @@
\isasymInter\index{$HOL3Set2@\isasymInter|bold}&
\ttindexbold{INT}, \ttindexbold{Inter} &
\verb$\<Inter>$\\
+\isactrlsup{\isacharasterisk}\index{$HOL4star@\isactrlsup{\isacharasterisk}|bold}&
+\verb$^*$\index{$HOL4star@\verb$^$\texttt{*}|bold} &
+\verb$\<^sup>*$\\
+\isasyminverse\index{$HOL4inv@\isasyminverse|bold}&
+\verb$^-1$\index{$HOL4inv@\verb$^-1$|bold} &
+\verb$\<inverse>$\\
\hline
\end{tabular}
\end{center}