# HG changeset patch
# User haftmann
# Date 1193987853 -3600
# Node ID 8d6b03eef9c940c85cb8243d3b3e1bc657f35ad7
# Parent  22d16596c3060321934e0efdf09c8ea113ad182d
tuned

diff -r 22d16596c306 -r 8d6b03eef9c9 ANNOUNCE
--- a/ANNOUNCE	Thu Nov 01 20:20:19 2007 +0100
+++ b/ANNOUNCE	Fri Nov 02 08:17:33 2007 +0100
@@ -30,27 +30,18 @@
 * Built-in Metis prover, external linkup for automated provers, and
 'sledgehammer' 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.
-
 * Second generation code generator for a subset of HOL, targeting SML,
 Haskell, and OCaml.
 
 * Command 'normal_form' and method 'normalization'
 for evaluating terms with free variables.
 
-* Improved support for arbitrary ML operations depending on the
-logical context.
+* Full list comprehension syntax.
 
 * Parallel loading of theories based on native multicore support in
 Poly/ML 5.1.
 
-* Improved algebraic capabilities by means of semiring normalization,
-Groebner bases and Ferrante/Rackoff algorithm.
+* Much improved algebraic capabilities, including Groebner bases.
 
 
 You may get Isabelle2007 from the following mirror sites: