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)'.