5375

1 
\appendix


2 


3 
\chapter{Appendix}


4 
\label{sec:Appendix}


5 


6 
\begin{figure}[htbp]


7 
\begin{center}

5581

8 
\begin{tabular}{lllll}

5375

9 
\hline


10 
\texttt{arities} &

5581

11 
\texttt{assumes} &


12 
\texttt{axclass} &

5375

13 
\texttt{binder} &

5581

14 
\texttt{classes} \\


15 
\texttt{constdefs} &


16 
\texttt{consts} &

5375

17 
\texttt{default} &

5581

18 
\texttt{defines} &


19 
\texttt{defs} \\

5375

20 
\texttt{end} &

5581

21 
\texttt{fixes} &


22 
\texttt{global} &


23 
\texttt{inductive} &


24 
\texttt{infixl} \\

5375

25 
\texttt{infixr} &


26 
\texttt{instance} &

5581

27 
\texttt{local} &


28 
\texttt{locale} &


29 
\texttt{mixfix} \\

5375

30 
\texttt{ML} &


31 
\texttt{MLtext} &

5581

32 
\texttt{nonterminals} &

5375

33 
\texttt{oracle} &

5581

34 
\texttt{output} \\

5375

35 
\texttt{path} &

5581

36 
\texttt{primrec} &


37 
\texttt{rules} &

5375

38 
\texttt{setup} &

5581

39 
\texttt{syntax} \\

5375

40 
\texttt{translations} &

5581

41 
\texttt{typedef} &


42 
\texttt{types} &&\\

5375

43 
\hline


44 
\end{tabular}


45 
\end{center}


46 
\caption{Keywords in theory files}


47 
\label{fig:keywords}


48 
\end{figure}


49 


50 
\begin{figure}[htbp]


51 
\begin{center}


52 
\begin{tabular}{lllll}


53 
\hline


54 
\texttt{ALL} &


55 
\texttt{case} &


56 
\texttt{div} &


57 
\texttt{dvd} &


58 
\texttt{else} \\


59 
\texttt{EX} &


60 
\texttt{if} &


61 
\texttt{in} &


62 
\texttt{INT} &


63 
\texttt{Int} \\


64 
\texttt{LEAST} &


65 
\texttt{let} &


66 
\texttt{mod} &


67 
\texttt{O} &


68 
\texttt{o} \\


69 
\texttt{of} &


70 
\texttt{op} &


71 
\texttt{PROP} &


72 
\texttt{SIGMA} &


73 
\texttt{then} \\


74 
\texttt{Times} &


75 
\texttt{UN} &


76 
\texttt{Un} &&\\


77 
\hline


78 
\end{tabular}


79 
\end{center}


80 
\caption{Reserved words in HOL}


81 
\label{fig:ReservedWords}


82 
\end{figure}
