1.1 --- a/ANNOUNCE	Tue Nov 06 09:46:05 2007 +0100
     1.2 +++ b/ANNOUNCE	Tue Nov 06 12:06:30 2007 +0100
     1.3 @@ -28,15 +28,12 @@
     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 +* Auto quickcheck: toplevel goals are tested for counterexamples
    1.10 +automatically when they are stated.
    1.11  
    1.12  * Second generation code generator for a subset of HOL, targeting SML,
    1.13  Haskell, and OCaml.
    1.14  
    1.15 -* Embedding of ML code into theories with static references to the
    1.16 -logical context (via antiquotations).
    1.17 -
    1.18  * Command 'normal_form' and method "normalization" for evaluating
    1.19  terms with free variables.
    1.20  
    1.21 @@ -44,6 +41,9 @@
    1.22  
    1.23  * Much improved algebraic capabilities, including Groebner bases.
    1.24  
    1.25 +* Embedding of ML code into theories with static references to the
    1.26 +logical context (via antiquotations).
    1.27 +
    1.28  * Parallel loading of theories based on native multicore support in
    1.29  Poly/ML 5.1.
    1.30