NEWS
changeset 14375 a545da363b23
parent 14361 ad2f5da643b4
child 14380 04b603a6f17d
--- 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