--- a/ANNOUNCE Fri Oct 26 22:10:44 2007 +0200
+++ b/ANNOUNCE Sat Oct 27 12:48:24 2007 +0200
@@ -27,14 +27,16 @@
* New 'class' package combination of axclass + locale interpretation.
+* Built-in Metis prover, external linkup for automated provers, and
+'sledghammer' command for automated proof synthesis.
+
+* Full list comprehension syntax.
+
* Various improvements in locale infrastructure (interpretation etc.)
* Various improvements of Isar language elements and related proof
tools.
-* Built-in Metis prover, external linkup for automated provers, and
-'sledghammer' command for automated proof synthesis.
-
* Second generation code-generator for a subset of HOL, targeting SML,
Haskell, and OCaml.