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