doc-src/TutorialI/appendix.tex
changeset 11450 1b02a6c4032f
parent 11203 881222d48777
child 12180 91c9f661b183
     1.1 --- a/doc-src/TutorialI/appendix.tex	Mon Jul 23 19:06:11 2001 +0200
     1.2 +++ b/doc-src/TutorialI/appendix.tex	Tue Jul 24 11:25:54 2001 +0200
     1.3 @@ -107,7 +107,7 @@
     1.4  \hline
     1.5  \end{tabular}
     1.6  \end{center}
     1.7 -\caption{Mathematical symbols, their \textsc{ascii}-equivalents and internal names}
     1.8 +\caption{Mathematical Symbols, Their \textsc{ascii}-Equivalents and Internal Names}
     1.9  \label{tab:ascii}
    1.10  \end{table}\indexbold{ASCII@\textsc{ascii} symbols}
    1.11  
    1.12 @@ -153,7 +153,7 @@
    1.13  \hline
    1.14  \end{tabular}
    1.15  \end{center}
    1.16 -\caption{Reserved words in HOL terms}
    1.17 +\caption{Reserved Words in HOL Terms}
    1.18  \label{tab:ReservedWords}
    1.19  \end{table}
    1.20  
    1.21 @@ -185,6 +185,6 @@
    1.22  %\hline
    1.23  %\end{tabular}
    1.24  %\end{center}
    1.25 -%\caption{Minor keywords in HOL theories}
    1.26 +%\caption{Minor Keywords in HOL Theories}
    1.27  %\label{tab:keywords}
    1.28  %\end{table}