doc-src/Tutorial/appendix.tex
changeset 15338 08519594b0e4
parent 15337 628d87767434
child 15339 a7b603bbc1e6
--- a/doc-src/Tutorial/appendix.tex	Mon Nov 29 11:12:19 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-\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}