doc-src/TutorialI/Types/numerics.tex
changeset 27093 66d6da816be7
parent 23525 c7ded89c2de0
child 30200 0db3a35eab01
child 30240 5b25fee0362c
     1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Sun Jun 08 14:30:07 2008 +0200
     1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Sun Jun 08 14:30:46 2008 +0200
     1.3 @@ -335,7 +335,7 @@
     1.4  The real numbers are, moreover, \textbf{complete}: every set of reals that
     1.5  is bounded above has a least upper bound.  Completeness distinguishes the
     1.6  reals from the rationals, for which the set $\{x\mid x^2<2\}$ has no least
     1.7 -upper bound.  (It could only be $\surd2$, which is irrational. The
     1.8 +upper bound.  (It could only be $\surd2$, which is irrational.) The
     1.9  formalization of completeness, which is complicated, 
    1.10  can be found in theory \texttt{RComplete} of directory
    1.11  \texttt{Real}.
    1.12 @@ -401,7 +401,7 @@
    1.13  function, \cdx{abs}. Type \isa{int} is an ordered ring.
    1.14  \item 
    1.15  \tcdx{field} and \tcdx{ordered_field}: a field extends a ring with the
    1.16 -multiplicative inverse (called simply \cdx{inverse} and division~(\isa{/}).
    1.17 +multiplicative inverse (called simply \cdx{inverse} and division~(\isa{/})).
    1.18  An ordered field is based on an ordered ring. Type \isa{complex} is a field, while type \isa{real} is an ordered field.
    1.19  \item 
    1.20  \tcdx{division_by_zero} includes all types where \isa{inverse 0 = 0}