# HG changeset patch
# User wenzelm
# Date 1191266392 -7200
# Node ID 513bb015b46976d0354b28902f34f190324aa5e8
# Parent  38577b4b1fde23cb37a721b2d984699849c6286a
added auto_quickcheck feature;

diff -r 38577b4b1fde -r 513bb015b469 NEWS
--- a/NEWS	Mon Oct 01 21:19:50 2007 +0200
+++ b/NEWS	Mon Oct 01 21:19:52 2007 +0200
@@ -529,6 +529,11 @@
 
 *** HOL ***
 
+* New "auto_quickcheck" feature tests outermost goal statements for
+potential counter-examples.  Controlled by ML references
+auto_quickcheck (default true) and auto_quickcheck_time_limit (default
+5000 milliseconds).
+
 * Internal reorganisation of `size' of datatypes: size theorems
 "foo.size" are no longer subsumed by "foo.simps" (but are still
 simplification rules by default!); theorems "prod.size" now named