1.1 --- a/doc-src/TutorialI/appendix.tex	Thu Jan 25 11:59:52 2001 +0100
     1.2 +++ b/doc-src/TutorialI/appendix.tex	Thu Jan 25 15:31:31 2001 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4  \chapter{Appendix}
     1.5  \label{sec:Appendix}
     1.6  
     1.7 -\begin{figure}[htbp]
     1.8 +\begin{table}[htbp]
     1.9  \begin{center}
    1.10  \begin{tabular}{|l|l|l|}
    1.11  \hline
    1.12 @@ -98,11 +98,13 @@
    1.13  \hline
    1.14  \end{tabular}
    1.15  \end{center}
    1.16 -\caption{Mathematical symbols, their ASCII-equivalents and ProofGeneral codes}
    1.17 -\label{fig:ascii}
    1.18 -\end{figure}\indexbold{ASCII symbols}
    1.19 +\caption{Mathematical symbols, their ASCII-equivalents and X-Symbol codes}
    1.20 +\label{tab:ascii}
    1.21 +\end{table}\indexbold{ASCII symbols}
    1.22  
    1.23 -\begin{figure}[htbp]
    1.24 +\input{Misc/document/appendix.tex}
    1.25 +
    1.26 +\begin{table}[htbp]
    1.27  \begin{center}
    1.28  \begin{tabular}{|lllllllll|}
    1.29  \hline
    1.30 @@ -143,11 +145,11 @@
    1.31  \end{tabular}
    1.32  \end{center}
    1.33  \caption{Reserved words in HOL terms}
    1.34 -\label{fig:ReservedWords}
    1.35 -\end{figure}
    1.36 +\label{tab:ReservedWords}
    1.37 +\end{table}
    1.38  
    1.39  
    1.40 -%\begin{figure}[htbp]
    1.41 +%\begin{table}[htbp]
    1.42  %\begin{center}
    1.43  %\begin{tabular}{|lllll|}
    1.44  %\hline
    1.45 @@ -175,5 +177,5 @@
    1.46  %\end{tabular}
    1.47  %\end{center}
    1.48  %\caption{Minor keywords in HOL theories}
    1.49 -%\label{fig:keywords}
    1.50 -%\end{figure}
    1.51 +%\label{tab:keywords}
    1.52 +%\end{table}