doc-src/Tutorial/appendix.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/appendix.tex	Wed Aug 26 16:57:49 1998 +0200
@@ -0,0 +1,75 @@
+\appendix
+
+\chapter{Appendix}
+\label{sec:Appendix}
+
+\begin{figure}[htbp]
+\begin{center}
+\begin{tabular}{|llll|}
+\hline
+\texttt{arities} &
+\texttt{binder} &
+\texttt{classes} &
+\texttt{consts} \\
+\texttt{default} &
+\texttt{defs} &
+\texttt{end} &
+\texttt{global} \\
+\texttt{infixl} &
+\texttt{infixr} &
+\texttt{instance} &
+\texttt{local} \\
+\texttt{mixfix} &
+\texttt{ML} &
+\texttt{MLtext} &
+\texttt{nonterminals} \\
+\texttt{oracle} &
+\texttt{output} &
+\texttt{path} &
+\texttt{rules} \\
+\texttt{setup} &
+\texttt{syntax} &
+\texttt{translations} &
+\texttt{types} \\
+\texttt{constdefs} &
+\texttt{axclass} &&\\
+\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}