# HG changeset patch
# User wenzelm
# Date 1212007830 -7200
# Node ID 739d239ba5140a30c644a8772b344f12d6dc7f5a
# Parent  616c553c7cf1942093ac71cb217923f891fa354c
prepared for Isabelle2008;

diff -r 616c553c7cf1 -r 739d239ba514 ANNOUNCE
--- a/ANNOUNCE	Wed May 28 22:13:31 2008 +0200
+++ b/ANNOUNCE	Wed May 28 22:50:30 2008 +0200
@@ -1,54 +1,15 @@
-Subject: Announcing Isabelle2007
+Subject: Announcing Isabelle2008
 To: isabelle-users@cl.cam.ac.uk
 
-Isabelle2007 is finally available.
-
-This release introduces fundamental changes over Isabelle2005, see the
-NEWS file in the distribution for more details.  Numerous existing
-concepts have been generalized and re-implemented based on novel
-system architecture.  New theories and proof tools have been added
-(mostly for HOL).  Some highlights are:
-
-* Support for nominal datatypes (binding structures) due to the
-HOL-Nominal logic.
-
-* General local theory infrastructure for specifications depending on
-parameters and assumptions (e.g. from locales, classes).
-
-* New basic specification elements 'definition', 'axiomatization',
-'abbreviation', 'notation'.
-
-* New version of 'inductive' package for inductive predicates;
-separate variant 'inductive_set'.
-
-* New 'function' package for general recursive function definitions.
+Isabelle2008 is now available.
 
-* New 'class' package combination of axclass + locale interpretation.
-
-* Built-in Metis prover, external linkup for automated provers, and
-'sledgehammer' command for automated proof synthesis.
-
-* 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.
+This release mostly consolidates Isabelle2007, see the NEWS file in
+the distribution for more details.  Some notable improvements are:
 
-* Command 'normal_form' and method "normalization" for evaluating
-terms with free variables.
-
-* Full list comprehension syntax for HOL.
-
-* 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.
+* ...
 
 
-You may get Isabelle2007 from the following mirror sites:
+You may get Isabelle2008 from the following mirror sites:
 
   Cambridge (UK)       http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
   Munich (Germany)     http://isabelle.in.tum.de/