\appendix
\chapter{Appendix}
\label{sec:Appendix}
\begin{figure}[htbp]
\begin{center}
\begin{tabular}{|llll|}
\hline
\texttt{arities} &
\texttt{binder} &
\texttt{classes} &
\texttt{consts} \\
\texttt{default} &
\texttt{defs} &
\texttt{end} &
\texttt{global} \\
\texttt{infixl} &
\texttt{infixr} &
\texttt{instance} &
\texttt{local} \\
\texttt{mixfix} &
\texttt{ML} &
\texttt{MLtext} &
\texttt{nonterminals} \\
\texttt{oracle} &
\texttt{output} &
\texttt{path} &
\texttt{rules} \\
\texttt{setup} &
\texttt{syntax} &
\texttt{translations} &
\texttt{types} \\
\texttt{constdefs} &
\texttt{axclass} &&\\
\hline
\end{tabular}
\end{center}
\caption{Keywords in theory files}
\label{fig:keywords}
\end{figure}
\begin{figure}[htbp]
\begin{center}
\begin{tabular}{|lllll|}
\hline
\texttt{ALL} &
\texttt{case} &
\texttt{div} &
\texttt{dvd} &
\texttt{else} \\
\texttt{EX} &
\texttt{if} &
\texttt{in} &
\texttt{INT} &
\texttt{Int} \\
\texttt{LEAST} &
\texttt{let} &
\texttt{mod} &
\texttt{O} &
\texttt{o} \\
\texttt{of} &
\texttt{op} &
\texttt{PROP} &
\texttt{SIGMA} &
\texttt{then} \\
\texttt{Times} &
\texttt{UN} &
\texttt{Un} &&\\
\hline
\end{tabular}
\end{center}
\caption{Reserved words in HOL}
\label{fig:ReservedWords}
\end{figure}