summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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|)}