NEWS
 changeset 6157 29942d3a1818 parent 6155 e387d188d0ca child 6174 9fb306ded7e5
```     1.1 --- a/NEWS	Wed Jan 27 17:11:12 1999 +0100
1.2 +++ b/NEWS	Wed Jan 27 17:11:39 1999 +0100
1.3 @@ -36,17 +36,17 @@
1.4  * There are now decision procedures for linear arithmetic over nat and int:
1.5
1.6  1. arith_tac copes with arbitrary formulae involving `=', `<', `<=', `+',
1.7 -`-', `Suc' and numerical constants; other subterms are treated as atomic;
1.8 -subformulae not involving type `nat' or `int' are ignored; quantified
1.9 -subformulae are ignored unless they are positive universal or negative
1.10 -existential. The tactic has to be invoked by hand and can be a little bit
1.11 -slow. In particular, the running time is exponential in the number of
1.12 -occurrences of `-' on `nat'.
1.13 +`-', `Suc', `min', `max' and numerical constants; other subterms are treated
1.14 +as atomic; subformulae not involving type `nat' or `int' are ignored;
1.15 +quantified subformulae are ignored unless they are positive universal or
1.16 +negative existential. The tactic has to be invoked by hand and can be a
1.17 +little bit slow. In particular, the running time is exponential in the number
1.18 +of occurrences of `min' and `max', and `-' on `nat'.
1.19
1.20  2. fast_arith_tac is a cut-down version of arith_tac: it only takes (negated)
1.21  (in)equalities among the premises and the conclusion into account (i.e. no
1.22 -compound formulae) and does not know about `-' on `nat'. It is fast and is
1.23 -used automatically by the simplifier.
1.24 +compound formulae) and does not know about `min' and `max', and `-' on
1.25 +`nat'. It is fast and is used automatically by the simplifier.
1.26
1.27  NB: At the moment, these decision procedures do not cope with mixed nat/int
1.28  formulae where the two parts interact, such as `m < n ==> int(m) < int(n)'.
```