5375

1 
\appendix


2 


3 
\chapter{Appendix}


4 
\label{sec:Appendix}


5 


6 
\begin{figure}[htbp]


7 
\begin{center}


8 
\begin{tabular}{llll}


9 
\hline


10 
\texttt{arities} &


11 
\texttt{binder} &


12 
\texttt{classes} &


13 
\texttt{consts} \\


14 
\texttt{default} &


15 
\texttt{defs} &


16 
\texttt{end} &


17 
\texttt{global} \\


18 
\texttt{infixl} &


19 
\texttt{infixr} &


20 
\texttt{instance} &


21 
\texttt{local} \\


22 
\texttt{mixfix} &


23 
\texttt{ML} &


24 
\texttt{MLtext} &


25 
\texttt{nonterminals} \\


26 
\texttt{oracle} &


27 
\texttt{output} &


28 
\texttt{path} &


29 
\texttt{rules} \\


30 
\texttt{setup} &


31 
\texttt{syntax} &


32 
\texttt{translations} &


33 
\texttt{types} \\


34 
\texttt{constdefs} &


35 
\texttt{axclass} &&\\


36 
\hline


37 
\end{tabular}


38 
\end{center}


39 
\caption{Keywords in theory files}


40 
\label{fig:keywords}


41 
\end{figure}


42 


43 
\begin{figure}[htbp]


44 
\begin{center}


45 
\begin{tabular}{lllll}


46 
\hline


47 
\texttt{ALL} &


48 
\texttt{case} &


49 
\texttt{div} &


50 
\texttt{dvd} &


51 
\texttt{else} \\


52 
\texttt{EX} &


53 
\texttt{if} &


54 
\texttt{in} &


55 
\texttt{INT} &


56 
\texttt{Int} \\


57 
\texttt{LEAST} &


58 
\texttt{let} &


59 
\texttt{mod} &


60 
\texttt{O} &


61 
\texttt{o} \\


62 
\texttt{of} &


63 
\texttt{op} &


64 
\texttt{PROP} &


65 
\texttt{SIGMA} &


66 
\texttt{then} \\


67 
\texttt{Times} &


68 
\texttt{UN} &


69 
\texttt{Un} &&\\


70 
\hline


71 
\end{tabular}


72 
\end{center}


73 
\caption{Reserved words in HOL}


74 
\label{fig:ReservedWords}


75 
\end{figure}
