doc-src/TutorialI/Types/numerics.tex
changeset 13996 a994b92ab1ea
parent 13983 afc0dadddaa4
child 14288 d149e3cbdb39
     1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Fri May 09 17:19:58 2003 +0200
     1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Fri May 09 18:00:30 2003 +0200
     1.3 @@ -28,7 +28,9 @@
     1.4  and multiplication by constant factors; subterms involving other operators
     1.5  are regarded as variables.  The procedure can be slow, especially if the
     1.6  subgoal to be proved involves subtraction over type \isa{nat}, which 
     1.7 -causes case splits.  
     1.8 +causes case splits.  On types \isa{nat} and \isa{int}, \methdx{arith}
     1.9 +can deal with quantifiers (this is known as ``Presburger Arithmetic''),
    1.10 +whereas on type \isa{real} it cannot.
    1.11  
    1.12  The simplifier reduces arithmetic expressions in other
    1.13  ways, such as dividing through by common factors.  For problems that lie
    1.14 @@ -480,4 +482,4 @@
    1.15  Theory \isa{Hyperreal} also defines transcendental functions such as sine,
    1.16  cosine, exponential and logarithm --- even the versions for type
    1.17  \isa{real}, because they are defined using nonstandard limits.%
    1.18 -\index{numbers|)}
    1.19 \ No newline at end of file
    1.20 +\index{numbers|)}