--- 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