NEWS

   (e.g. genuiely long arrows)
 
 *** 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 ***
 
 * tuned current_goals_markers semantics: begin / end goal avoids
 printing empty lines;