diff -r 0d52e7cbff29 -r 29942d3a1818 NEWS
--- a/NEWS	Wed Jan 27 17:11:12 1999 +0100
+++ b/NEWS	Wed Jan 27 17:11:39 1999 +0100
@@ -36,17 +36,17 @@
 * There are now decision procedures for linear arithmetic over nat and int:
 
 1. arith_tac copes with arbitrary formulae involving `=', `<', `<=', `+',
-`-', `Suc' and numerical constants; other subterms are treated as atomic;
-subformulae not involving type `nat' or `int' are ignored; quantified
-subformulae are ignored unless they are positive universal or negative
-existential. The tactic has to be invoked by hand and can be a little bit
-slow. In particular, the running time is exponential in the number of
-occurrences of `-' on `nat'.
+`-', `Suc', `min', `max' and numerical constants; other subterms are treated
+as atomic; subformulae not involving type `nat' or `int' are ignored;
+quantified subformulae are ignored unless they are positive universal or
+negative existential. The tactic has to be invoked by hand and can be a
+little bit slow. In particular, the running time is exponential in the number
+of occurrences of `min' and `max', and `-' on `nat'.
 
 2. fast_arith_tac is a cut-down version of arith_tac: it only takes (negated)
 (in)equalities among the premises and the conclusion into account (i.e. no
-compound formulae) and does not know about `-' on `nat'. It is fast and is
-used automatically by the simplifier.
+compound formulae) and does not know about `min' and `max', and `-' on
+`nat'. It is fast and is used automatically by the simplifier.
 
 NB: At the moment, these decision procedures do not cope with mixed nat/int
 formulae where the two parts interact, such as `m < n ==> int(m) < int(n)'.