ANNOUNCE
changeset 25305 574c4964fe54
parent 25271 f28efd37e18a
child 25306 351ca94cabdb
     1.1 --- a/ANNOUNCE	Tue Nov 06 08:47:30 2007 +0100
     1.2 +++ b/ANNOUNCE	Tue Nov 06 09:46:05 2007 +0100
     1.3 @@ -28,6 +28,9 @@
     1.4  * Built-in Metis prover, external linkup for automated provers, and
     1.5  'sledgehammer' command for automated proof synthesis.
     1.6  
     1.7 +* Autoquickcheck: lemmas are tested for counterexamples
     1.8 +automatically when they are stated. 
     1.9 +
    1.10  * Second generation code generator for a subset of HOL, targeting SML,
    1.11  Haskell, and OCaml.
    1.12