# HG changeset patch
# User haftmann
# Date 1194338765 -3600
# Node ID 574c4964fe547ac5da10aeec1aa49bb11fed9251
# Parent  7491c00f0915d99037a58e7c00faa94a780b1009
added autoquickcheck

diff -r 7491c00f0915 -r 574c4964fe54 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.