1.1 --- a/NEWS	Mon Jan 04 15:08:40 1999 +0100
     1.2 +++ b/NEWS	Mon Jan 04 16:13:57 1999 +0100
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 @@ -9,6 +8,13 @@
     1.9  
    1.10  * HOL: Removed the obsolete syntax "Compl A"; use -A for set complement
    1.11  
    1.12 +*** Proof tools ***
    1.13 +
    1.14 +* Provers/Arith/fast_lin_arith.ML contains a functor for creating a decision
    1.15 +procedure for linear arithmetic. Currently it is used only for type `nat' in
    1.16 +HOL (see below) but can, should and will be instantiated for other types and
    1.17 +logics as well.
    1.18 +
    1.19  *** General ***
    1.20  
    1.21  * in locales, the "assumes" and "defines" parts may be omitted if empty;
    1.22 @@ -16,6 +22,17 @@
    1.23  * new print_mode "xsymbols" for extended symbol support 
    1.24    (e.g. genuiely long arrows)
    1.25  
    1.26 +*** HOL ***
    1.27 +
    1.28 +* There are now two decision procedures for linear arithmetic over nat:
    1.29 +1. nat_arith_tac copes with arbitrary propositional formulae (quantified
    1.30 +formulae are treated as atomic) involving `=', `<', `<=', 0, Suc, `+' and `-'
    1.31 +(other operators are treated as atomic). It has to be invoked by hand and is
    1.32 +a little bit slow.
    1.33 +2. fast_nat_arith_tac is a cut-down version of nat_arith_tac: it does not do
    1.34 +much propositional reasoning (hence the premises and the conclusion should be
    1.35 +as atomic as possible) and does not know about `-' either. It is fast and is
    1.36 +used automatically by the simplifier.
    1.37  
    1.38  *** Internal programming interfaces ***
    1.39