--- a/doc-src/TutorialI/Types/numerics.tex Mon Mar 19 13:28:06 2001 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Mon Mar 19 17:25:42 2001 +0100
@@ -87,7 +87,7 @@
-\subsection{The type of natural numbers, {\tt\slshape nat}}
+\subsection{The Type of Natural Numbers, {\tt\slshape nat}}
This type requires no introduction: we have been using it from the
beginning. Hundreds of theorems about the natural numbers are
@@ -198,7 +198,7 @@
\rulename{dvd_add}
\end{isabelle}
-\subsubsection{Simplifier tricks}
+\subsubsection{Simplifier Tricks}
The rule \isa{diff_mult_distrib} shown above is one of the few facts
about \isa{m\ -\ n} that is not subject to
the condition \isa{n\ \isasymle \ m}. Natural number subtraction has few
@@ -251,7 +251,7 @@
\end{isabelle}
-\subsection{The type of integers, {\tt\slshape int}}
+\subsection{The Type of Integers, {\tt\slshape int}}
Reasoning methods resemble those for the natural numbers, but induction and
the constant \isa{Suc} are not available. HOL provides many lemmas
@@ -333,7 +333,7 @@
\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.
-\subsection{The type of real numbers, {\tt\slshape real}}
+\subsection{The Type of Real Numbers, {\tt\slshape real}}
The real numbers enjoy two significant properties that the integers lack.
They are