equal
deleted
inserted
replaced
96 \verb$^-1$\index{$HOL4inv@\verb$^-1$|bold} & |
96 \verb$^-1$\index{$HOL4inv@\verb$^-1$|bold} & |
97 \verb$\<inverse>$\\ |
97 \verb$\<inverse>$\\ |
98 \hline |
98 \hline |
99 \end{tabular} |
99 \end{tabular} |
100 \end{center} |
100 \end{center} |
101 \caption{Mathematical symbols, their \textsc{ascii}-equivalents and X-symbol codes} |
101 \caption{Mathematical symbols, their \textsc{ascii}-equivalents and internal names} |
102 \label{tab:ascii} |
102 \label{tab:ascii} |
103 \end{table}\indexbold{ASCII@\textsc{ascii} symbols} |
103 \end{table}\indexbold{ASCII@\textsc{ascii} symbols} |
104 |
104 |
105 \input{Misc/document/appendix.tex} |
105 \input{Misc/document/appendix.tex} |
106 |
106 |