# HG changeset patch
# User nipkow
# Date 915553807 -3600
# Node ID aa2ac7d217921decc61909a78d2617f13ad924b6
# Parent  ede9fea461f5158489f9eb83466b0917e23a880e
*** empty log message ***

diff -r ede9fea461f5 -r aa2ac7d21792 NEWS
--- a/NEWS	Tue Jan 05 17:28:46 1999 +0100
+++ b/NEWS	Tue Jan 05 17:30:07 1999 +0100
@@ -11,9 +11,9 @@
 *** Proof tools ***
 
 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a decision
-procedure for linear arithmetic. Currently it is used only for type `nat' in
-HOL (see below) but can, should and will be instantiated for other types and
-logics as well.
+procedure for linear arithmetic. Currently it is used for types `nat' and
+`int' in HOL (see below) but can, should and will be instantiated for other
+types and logics as well.
 
 *** General ***
 
@@ -24,15 +24,23 @@
 
 *** HOL ***
 
-* There are now two decision procedures for linear arithmetic over nat:
-1. nat_arith_tac copes with arbitrary propositional formulae (quantified
-formulae are treated as atomic) involving `=', `<', `<=', 0, Suc, `+' and `-'
-(other operators are treated as atomic). It has to be invoked by hand and is
-a little bit slow.
-2. fast_nat_arith_tac is a cut-down version of nat_arith_tac: it does not do
-much propositional reasoning (hence the premises and the conclusion should be
-as atomic as possible) and does not know about `-' either. It is fast and is
+* 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
 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)'.
 
 *** Internal programming interfaces ***