# HG changeset patch
# User wenzelm
# Date 1194347190 -3600
# Node ID 351ca94cabdb6db7eb5a073d19934a6ab8d96a72
# Parent  574c4964fe547ac5da10aeec1aa49bb11fed9251
tuned;

diff -r 574c4964fe54 -r 351ca94cabdb ANNOUNCE
--- a/ANNOUNCE	Tue Nov 06 09:46:05 2007 +0100
+++ b/ANNOUNCE	Tue Nov 06 12:06:30 2007 +0100
@@ -28,15 +28,12 @@
 * 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. 
+* Auto quickcheck: toplevel goals are tested for counterexamples
+automatically when they are stated.
 
 * Second generation code generator for a subset of HOL, targeting SML,
 Haskell, and OCaml.
 
-* Embedding of ML code into theories with static references to the
-logical context (via antiquotations).
-
 * Command 'normal_form' and method "normalization" for evaluating
 terms with free variables.
 
@@ -44,6 +41,9 @@
 
 * Much improved algebraic capabilities, including Groebner bases.
 
+* Embedding of ML code into theories with static references to the
+logical context (via antiquotations).
+
 * Parallel loading of theories based on native multicore support in
 Poly/ML 5.1.