NEWS
changeset 13881 f63e2a057fd4
parent 13872 601514e63534
child 13899 12c7029d278b
     1.1 --- a/NEWS	Tue Mar 25 09:50:53 2003 +0100
     1.2 +++ b/NEWS	Tue Mar 25 09:52:21 2003 +0100
     1.3 @@ -131,6 +131,11 @@
     1.4  
     1.5    "n div 2 + (n+1) div 2 = (n::nat)"
     1.6  
     1.7 +* New method / tactic presburger(_tac) for full Presburger arithmetic
     1.8 +  (by Amine Chaieb). Integrated with arith(_tac), i.e. presburger(_tac)
     1.9 +  is called automatically by arith(_tac), if the decision procedure for
    1.10 +  simple arithmetic fails to solve the goal.
    1.11 +
    1.12  * simp's arithmetic capabilities have been enhanced a bit: it now
    1.13  takes ~= in premises into account (by performing a case split);
    1.14