1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/Tutorial/appendix.tex	Wed Aug 26 16:57:49 1998 +0200
     1.3 @@ -0,0 +1,75 @@
     1.4 +\appendix
     1.5 +
     1.6 +\chapter{Appendix}
     1.7 +\label{sec:Appendix}
     1.8 +
     1.9 +\begin{figure}[htbp]
    1.10 +\begin{center}
    1.11 +\begin{tabular}{|llll|}
    1.12 +\hline
    1.13 +\texttt{arities} &
    1.14 +\texttt{binder} &
    1.15 +\texttt{classes} &
    1.16 +\texttt{consts} \\
    1.17 +\texttt{default} &
    1.18 +\texttt{defs} &
    1.19 +\texttt{end} &
    1.20 +\texttt{global} \\
    1.21 +\texttt{infixl} &
    1.22 +\texttt{infixr} &
    1.23 +\texttt{instance} &
    1.24 +\texttt{local} \\
    1.25 +\texttt{mixfix} &
    1.26 +\texttt{ML} &
    1.27 +\texttt{MLtext} &
    1.28 +\texttt{nonterminals} \\
    1.29 +\texttt{oracle} &
    1.30 +\texttt{output} &
    1.31 +\texttt{path} &
    1.32 +\texttt{rules} \\
    1.33 +\texttt{setup} &
    1.34 +\texttt{syntax} &
    1.35 +\texttt{translations} &
    1.36 +\texttt{types} \\
    1.37 +\texttt{constdefs} &
    1.38 +\texttt{axclass} &&\\
    1.39 +\hline
    1.40 +\end{tabular}
    1.41 +\end{center}
    1.42 +\caption{Keywords in theory files}
    1.43 +\label{fig:keywords}
    1.44 +\end{figure}
    1.45 +
    1.46 +\begin{figure}[htbp]
    1.47 +\begin{center}
    1.48 +\begin{tabular}{|lllll|}
    1.49 +\hline
    1.50 +\texttt{ALL} &
    1.51 +\texttt{case} &
    1.52 +\texttt{div} &
    1.53 +\texttt{dvd} &
    1.54 +\texttt{else} \\
    1.55 +\texttt{EX} &
    1.56 +\texttt{if} &
    1.57 +\texttt{in} &
    1.58 +\texttt{INT} &
    1.59 +\texttt{Int} \\
    1.60 +\texttt{LEAST} &
    1.61 +\texttt{let} &
    1.62 +\texttt{mod} &
    1.63 +\texttt{O} &
    1.64 +\texttt{o} \\
    1.65 +\texttt{of} &
    1.66 +\texttt{op} &
    1.67 +\texttt{PROP} &
    1.68 +\texttt{SIGMA} &
    1.69 +\texttt{then} \\
    1.70 +\texttt{Times} &
    1.71 +\texttt{UN} &
    1.72 +\texttt{Un} &&\\
    1.73 +\hline
    1.74 +\end{tabular}
    1.75 +\end{center}
    1.76 +\caption{Reserved words in HOL}
    1.77 +\label{fig:ReservedWords}
    1.78 +\end{figure}