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

5850

10 
\texttt{and} &

5375

11 
\texttt{arities} &

5581

12 
\texttt{assumes} &


13 
\texttt{axclass} &

5850

14 
\texttt{binder} \\


15 
\texttt{classes} &

5581

16 
\texttt{constdefs} &


17 
\texttt{consts} &

5375

18 
\texttt{default} &

5850

19 
\texttt{defines} \\


20 
\texttt{defs} &

5375

21 
\texttt{end} &

5581

22 
\texttt{fixes} &


23 
\texttt{global} &

5850

24 
\texttt{inductive} \\


25 
\texttt{infixl} &

5375

26 
\texttt{infixr} &


27 
\texttt{instance} &

5581

28 
\texttt{local} &

5850

29 
\texttt{locale} \\


30 
\texttt{mixfix} &

5375

31 
\texttt{ML} &


32 
\texttt{MLtext} &

5581

33 
\texttt{nonterminals} &

5850

34 
\texttt{oracle} \\


35 
\texttt{output} &

5375

36 
\texttt{path} &

5581

37 
\texttt{primrec} &


38 
\texttt{rules} &

5850

39 
\texttt{setup} \\


40 
\texttt{syntax} &

5375

41 
\texttt{translations} &

5581

42 
\texttt{typedef} &

5850

43 
\texttt{types} &\\

5375

44 
\hline


45 
\end{tabular}


46 
\end{center}


47 
\caption{Keywords in theory files}


48 
\label{fig:keywords}


49 
\end{figure}


50 


51 
\begin{figure}[htbp]


52 
\begin{center}


53 
\begin{tabular}{lllll}


54 
\hline


55 
\texttt{ALL} &


56 
\texttt{case} &


57 
\texttt{div} &


58 
\texttt{dvd} &


59 
\texttt{else} \\


60 
\texttt{EX} &


61 
\texttt{if} &


62 
\texttt{in} &


63 
\texttt{INT} &


64 
\texttt{Int} \\


65 
\texttt{LEAST} &


66 
\texttt{let} &


67 
\texttt{mod} &


68 
\texttt{O} &


69 
\texttt{o} \\


70 
\texttt{of} &


71 
\texttt{op} &


72 
\texttt{PROP} &


73 
\texttt{SIGMA} &


74 
\texttt{then} \\


75 
\texttt{Times} &


76 
\texttt{UN} &


77 
\texttt{Un} &&\\


78 
\hline


79 
\end{tabular}


80 
\end{center}


81 
\caption{Reserved words in HOL}


82 
\label{fig:ReservedWords}


83 
\end{figure}
