doc-src/Tutorial/appendix.tex

clarified eq_thm;
added eq_thm_prop;

\appendix

\chapter{Appendix}
\label{sec:Appendix}

\begin{figure}[htbp]
\begin{center}
\begin{tabular}{|lllll|}
\hline
\texttt{and} &
\texttt{arities} &
\texttt{assumes} &
\texttt{axclass} &
\texttt{binder} \\
\texttt{classes} &
\texttt{constdefs} &
\texttt{consts} &
\texttt{default} &
\texttt{defines} \\
\texttt{defs} &
\texttt{end} &
\texttt{fixes} &
\texttt{global} &
\texttt{inductive} \\
\texttt{infixl} &
\texttt{infixr} &
\texttt{instance} &
\texttt{local} &
\texttt{locale} \\
\texttt{mixfix} &
\texttt{ML} &
\texttt{MLtext} &
\texttt{nonterminals} &
\texttt{oracle} \\
\texttt{output} &
\texttt{path} &
\texttt{primrec} &
\texttt{rules} &
\texttt{setup} \\
\texttt{syntax} &
\texttt{translations} &
\texttt{typedef} &
\texttt{types} &\\
\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}