*** empty log message ***

--- a/NEWS	Tue Aug 13 21:57:15 2002 +0200
+++ b/NEWS	Tue Aug 13 21:59:44 2002 +0200
@@ -40,6 +40,9 @@
 * attribute [symmetric] now works for relations as well; it turns
 (x,y) : R^-1 into (y,x) : R, and vice versa;
 
+* arith(_tac) now produces a counter example if it cannot prove a theorem.
+  In ProofGeneral the counter example appears in the trace buffer.
+
 * arith(_tac) does now know about div k and mod k where k is a numeral
 of type nat or int. It can solve simple goals like