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