diff -r 3b7e2dbbd684 -r 320a1d67b9ae NEWS
--- a/NEWS	Tue Oct 27 12:59:57 2009 +0000
+++ b/NEWS	Tue Oct 27 14:46:03 2009 +0000
@@ -50,6 +50,9 @@
 this method is proof-producing. Certificates are provided to
 avoid calling the external solvers solely for re-checking proofs.
 
+* New counterexample generator tool "nitpick" based on the Kodkod
+relational model finder.
+
 * Reorganization of number theory:
   * former session NumberTheory now named Old_Number_Theory
   * new session Number_Theory by Jeremy Avigad; if possible, prefer this.
@@ -167,7 +170,8 @@
 
 * New implementation of quickcheck uses generic code generator;
 default generators are provided for all suitable HOL types, records
-and datatypes.
+and datatypes.  Old quickcheck can be re-activated importing
+theory Library/SML_Quickcheck.
 
 * Renamed theorems:
 Suc_eq_add_numeral_1 -> Suc_eq_plus1