doc-src/TutorialI/appendix.tex

 \appendix
 
 \chapter{Appendix}
 \label{sec:Appendix}
 
-\begin{figure}[htbp]
+\begin{table}[htbp]
 \begin{center}
 \begin{tabular}{|l|l|l|}
 \hline
 \indexboldpos{\isasymlbrakk}{$Isabrl} &
 \texttt{[|}\index{$Isabrl@\ttlbr|bold} &

 \verb$^-1$\index{$HOL4inv@\verb$^-1$|bold} &
 \verb$\<inverse>$\\
 \hline
 \end{tabular}
 \end{center}
-\caption{Mathematical symbols, their ASCII-equivalents and ProofGeneral codes}
-\label{fig:ascii}
-\end{figure}\indexbold{ASCII symbols}
+\caption{Mathematical symbols, their ASCII-equivalents and X-Symbol codes}
+\label{tab:ascii}
+\end{table}\indexbold{ASCII symbols}
 
-\begin{figure}[htbp]
+\input{Misc/document/appendix.tex}
+
+\begin{table}[htbp]
 \begin{center}
 \begin{tabular}{|lllllllll|}
 \hline
 \texttt{ALL} &
 \texttt{BIT} &

 \texttt{then}&&\\
 \hline
 \end{tabular}
 \end{center}
 \caption{Reserved words in HOL terms}
-\label{fig:ReservedWords}
-\end{figure}
+\label{tab:ReservedWords}
+\end{table}
 
 
-%\begin{figure}[htbp]
+%\begin{table}[htbp]
 %\begin{center}
 %\begin{tabular}{|lllll|}
 %\hline
 %\texttt{and} &
 %\texttt{binder} &

 % \\
 %\hline
 %\end{tabular}
 %\end{center}
 %\caption{Minor keywords in HOL theories}
-%\label{fig:keywords}
-%\end{figure}
+%\label{tab:keywords}
+%\end{table}