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