*** empty log message ***
authornipkow
Wed, 04 Feb 2004 03:44:05 +0100
changeset 14375 a545da363b23
parent 14374 61de62096768
child 14376 9fe787a90a48
*** empty log message ***
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