tuned
authorhaftmann
Fri Nov 02 08:17:33 2007 +0100 (2007-11-02)
changeset 252598d6b03eef9c9
parent 25258 22d16596c306
child 25260 71b2a1fefb84
tuned
ANNOUNCE
     1.1 --- a/ANNOUNCE	Thu Nov 01 20:20:19 2007 +0100
     1.2 +++ b/ANNOUNCE	Fri Nov 02 08:17:33 2007 +0100
     1.3 @@ -30,27 +30,18 @@
     1.4  * Built-in Metis prover, external linkup for automated provers, and
     1.5  'sledgehammer' command for automated proof synthesis.
     1.6  
     1.7 -* Full list comprehension syntax.
     1.8 -
     1.9 -* Various improvements in locale infrastructure (interpretation etc.)
    1.10 -
    1.11 -* Various improvements of Isar language elements and related proof
    1.12 -tools.
    1.13 -
    1.14  * Second generation code generator for a subset of HOL, targeting SML,
    1.15  Haskell, and OCaml.
    1.16  
    1.17  * Command 'normal_form' and method 'normalization'
    1.18  for evaluating terms with free variables.
    1.19  
    1.20 -* Improved support for arbitrary ML operations depending on the
    1.21 -logical context.
    1.22 +* Full list comprehension syntax.
    1.23  
    1.24  * Parallel loading of theories based on native multicore support in
    1.25  Poly/ML 5.1.
    1.26  
    1.27 -* Improved algebraic capabilities by means of semiring normalization,
    1.28 -Groebner bases and Ferrante/Rackoff algorithm.
    1.29 +* Much improved algebraic capabilities, including Groebner bases.
    1.30  
    1.31  
    1.32  You may get Isabelle2007 from the following mirror sites: