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

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