# HG changeset patch
# User nipkow
# Date 1075862645 -3600
# Node ID a545da363b23a8f53648817544caa16be7cad80b
# Parent  61de6209676840b8657f8974e6ecc45fff37cead
*** empty log message ***

diff -r 61de62096768 -r a545da363b23 NEWS
--- a/NEWS	Tue Feb 03 15:58:31 2004 +0100
+++ b/NEWS	Wed Feb 04 03:44:05 2004 +0100
@@ -89,6 +89,9 @@
   specification.  There is also an 'ax_specification' command that
   introduces the new constants axiomatically.
 
+
+* arith(_tac) is now able to generate counterexamples for reals as well.
+
 * SET-Protocol: formalization and verification of the SET protocol suite;
 
 * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function