ANNOUNCE

--- a/ANNOUNCE	Tue Nov 06 08:47:30 2007 +0100
+++ b/ANNOUNCE	Tue Nov 06 09:46:05 2007 +0100
@@ -28,6 +28,9 @@
 * Built-in Metis prover, external linkup for automated provers, and
 'sledgehammer' command for automated proof synthesis.
 
+* Autoquickcheck: lemmas are tested for counterexamples
+automatically when they are stated. 
+
 * Second generation code generator for a subset of HOL, targeting SML,
 Haskell, and OCaml.