Revising the Client proof as suggested by Michel Charpentier. New lemmas
about composition (in Union.ML), etc. Also changed "length" to "size"
because it is displayed as "size" in any event.
\appendix
\chapter{Appendix}
\label{sec:Appendix}
\begin{figure}[htbp]
\begin{center}
\begin{tabular}{|lllll|}
\hline
\texttt{arities} &
\texttt{assumes} &
\texttt{axclass} &
\texttt{binder} &
\texttt{classes} \\
\texttt{constdefs} &
\texttt{consts} &
\texttt{default} &
\texttt{defines} &
\texttt{defs} \\
\texttt{end} &
\texttt{fixes} &
\texttt{global} &
\texttt{inductive} &
\texttt{infixl} \\
\texttt{infixr} &
\texttt{instance} &
\texttt{local} &
\texttt{locale} &
\texttt{mixfix} \\
\texttt{ML} &
\texttt{MLtext} &
\texttt{nonterminals} &
\texttt{oracle} &
\texttt{output} \\
\texttt{path} &
\texttt{primrec} &
\texttt{rules} &
\texttt{setup} &
\texttt{syntax} \\
\texttt{translations} &
\texttt{typedef} &
\texttt{types} &&\\
\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}