doc-src/TutorialI/Types/numerics.tex
 changeset 11216 279004936bb0 parent 11174 96a533d300a6 child 11389 55e2aef8909b
     1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Mon Mar 19 13:28:06 2001 +0100
1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Mon Mar 19 17:25:42 2001 +0100
1.3 @@ -87,7 +87,7 @@
1.4
1.5
1.6
1.7 -\subsection{The type of natural numbers, {\tt\slshape nat}}
1.8 +\subsection{The Type of Natural Numbers, {\tt\slshape nat}}
1.9
1.10  This type requires no introduction: we have been using it from the
1.11  beginning.  Hundreds of theorems about the natural numbers are
1.12 @@ -198,7 +198,7 @@
1.14  \end{isabelle}
1.15
1.16 -\subsubsection{Simplifier tricks}
1.17 +\subsubsection{Simplifier Tricks}
1.18  The rule \isa{diff_mult_distrib} shown above is one of the few facts
1.19  about \isa{m\ -\ n} that is not subject to
1.20  the condition \isa{n\ \isasymle \  m}.  Natural number subtraction has few
1.21 @@ -251,7 +251,7 @@
1.22  \end{isabelle}
1.23
1.24
1.25 -\subsection{The type of integers, {\tt\slshape int}}
1.26 +\subsection{The Type of Integers, {\tt\slshape int}}
1.27
1.28  Reasoning methods resemble those for the natural numbers, but induction and
1.29  the constant \isa{Suc} are not available.  HOL provides many lemmas
1.30 @@ -333,7 +333,7 @@
1.31  \isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.
1.32
1.33
1.34 -\subsection{The type of real numbers, {\tt\slshape real}}
1.35 +\subsection{The Type of Real Numbers, {\tt\slshape real}}
1.36
1.37  The real numbers enjoy two significant properties that the integers lack.
1.38  They are