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.13  \rulename{dvd_add}
    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