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