--- a/NEWS Thu Jan 14 13:20:02 1999 +0100
+++ b/NEWS Thu Jan 14 14:29:52 1999 +0100
@@ -30,22 +30,22 @@
*** HOL ***
* There are now decision procedures for linear arithmetic over nat and int:
-1. nat_arith_tac copes with arbitrary formulae involving `=', `<', `<=', 0,
-Suc, `+' and `-'; other subterms are treated as atomic; subformulae not
-involving type `nat' 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 `-'.
-2. fast_nat_arith_tac is a cut-down version of nat_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 `-'. It is fast and is
+
+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'.
+
+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.
-3. int_arith_tac behaves like nat_arith_tac but applies to inequalities over
-`int'; it also knows about unary `-'; binary `-' does not cause a blow-up.
-4. fast_int_arith_tac is related to int_arith_tac like fast_nat_arith_tac is
-related to nat_arith_tac.
+
NB: At the moment, these decision procedures do not cope with mixed nat/int
-formulae such as `m < n ==> int(m) < int(n)'.
+formulae where the two parts interact, such as `m < n ==> int(m) < int(n)'.
*** Internal programming interfaces ***