--- a/doc-src/TutorialI/appendix.tex Mon Jul 23 19:06:11 2001 +0200
+++ b/doc-src/TutorialI/appendix.tex Tue Jul 24 11:25:54 2001 +0200
@@ -107,7 +107,7 @@
\hline
\end{tabular}
\end{center}
-\caption{Mathematical symbols, their \textsc{ascii}-equivalents and internal names}
+\caption{Mathematical Symbols, Their \textsc{ascii}-Equivalents and Internal Names}
\label{tab:ascii}
\end{table}\indexbold{ASCII@\textsc{ascii} symbols}
@@ -153,7 +153,7 @@
\hline
\end{tabular}
\end{center}
-\caption{Reserved words in HOL terms}
+\caption{Reserved Words in HOL Terms}
\label{tab:ReservedWords}
\end{table}
@@ -185,6 +185,6 @@
%\hline
%\end{tabular}
%\end{center}
-%\caption{Minor keywords in HOL theories}
+%\caption{Minor Keywords in HOL Theories}
%\label{tab:keywords}
%\end{table}