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