# HG changeset patch
# User nipkow
# Date 1029268784 -7200
# Node ID 2222c7a0e8bb80d0fbbae7e22287ca3042b70609
# Parent  f95f5818f24f1913840c24bd06813e042191d5d5
*** empty log message ***

diff -r f95f5818f24f -r 2222c7a0e8bb NEWS
--- 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