# HG changeset patch
# User berghofe
# Date 1048582341 -3600
# Node ID f63e2a057fd4baf68a89c2a37e39057e42108f84
# Parent  4f7f30f6892629b7b763e18eac76fc25c09f6d48
Presburger arithmetic

diff -r 4f7f30f68926 -r f63e2a057fd4 NEWS
--- a/NEWS	Tue Mar 25 09:50:53 2003 +0100
+++ b/NEWS	Tue Mar 25 09:52:21 2003 +0100
@@ -131,6 +131,11 @@
 
   "n div 2 + (n+1) div 2 = (n::nat)"
 
+* New method / tactic presburger(_tac) for full Presburger arithmetic
+  (by Amine Chaieb). Integrated with arith(_tac), i.e. presburger(_tac)
+  is called automatically by arith(_tac), if the decision procedure for
+  simple arithmetic fails to solve the goal.
+
 * simp's arithmetic capabilities have been enhanced a bit: it now
 takes ~= in premises into account (by performing a case split);