
diff -r b44ad7e4c4d2 -r 279004936bb0 doc-src/TutorialI/Types/numerics.tex
--- 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




