changeset 25259 8d6b03eef9c9
parent 25242 6c3890cbceac
child 25271 f28efd37e18a
--- 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
 * 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: