doc-src/TutorialI/appendix.tex
changeset 10801 c00ac928fc6f
parent 10654 458068404143
child 10978 5eebea8f359f
     1.1 --- a/doc-src/TutorialI/appendix.tex	Sat Jan 06 11:27:09 2001 +0100
     1.2 +++ b/doc-src/TutorialI/appendix.tex	Sat Jan 06 12:39:05 2001 +0100
     1.3 @@ -89,6 +89,12 @@
     1.4  \isasymInter\index{$HOL3Set2@\isasymInter|bold}&
     1.5  \ttindexbold{INT}, \ttindexbold{Inter} &
     1.6  \verb$\<Inter>$\\
     1.7 +\isactrlsup{\isacharasterisk}\index{$HOL4star@\isactrlsup{\isacharasterisk}|bold}&
     1.8 +\verb$^*$\index{$HOL4star@\verb$^$\texttt{*}|bold} &
     1.9 +\verb$\<^sup>*$\\
    1.10 +\isasyminverse\index{$HOL4inv@\isasyminverse|bold}&
    1.11 +\verb$^-1$\index{$HOL4inv@\verb$^-1$|bold} &
    1.12 +\verb$\<inverse>$\\
    1.13  \hline
    1.14  \end{tabular}
    1.15  \end{center}