# HG changeset patch
# User wenzelm
# Date 1275038614 -7200
# Node ID 07f3f5a03e98117f68c4152ffca1fdc7cd02b21d
# Parent  c96e119b7fe963c7f64d0754b5008d5c32c7435c
some updates for release;

diff -r c96e119b7fe9 -r 07f3f5a03e98 ANNOUNCE
--- a/ANNOUNCE	Thu May 27 21:37:42 2010 +0200
+++ b/ANNOUNCE	Fri May 28 11:23:34 2010 +0200
@@ -1,48 +1,16 @@
-Subject: Announcing Isabelle2009-1
+Subject: Announcing Isabelle2009-2
 To: isabelle-users@cl.cam.ac.uk
 
-Isabelle2009-1 is now available.
+Isabelle2009-2 is now available.
 
-This release improves upon Isabelle2009 in many ways, see the NEWS
-file in the distribution for more details.  Some important changes
+This release improves upon Isabelle2009-1 in many respects, see the
+NEWS file in the distribution for more details.  Some notable changes
 are:
 
-* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
-on a given logic image.
-
-* HOL-SMT: proof method "smt" for a combination of first-order logic
-with equality, linear and nonlinear (natural/integer/real) arithmetic,
-and fixed-size bitvectors.
-
-* HOL-Boogie: an interactive prover back-end for Boogie and VCC.
-
-* HOL: counterexample generator tool Nitpick based on the Kodkod
-relational model finder.
-
-* HOL: predicate compiler turning inductive into (executable)
-equational specifications.
-
-* HOL: refined number theory.
-
-* HOL: various parts of multivariate analysis.
-
-* HOL-Library: proof method "sos" (sum of squares) for nonlinear real
-arithmetic, based on external semidefinite programming solvers.
-
-* HOLCF: new definitional domain package.
-
-* Revised tutorial on locales.
-
-* ML: tacticals for subgoal focus.
-
-* ML: support for Poly/ML 5.3.0, with improved reporting of compiler
-errors and run-time exceptions, including detailed source positions.
-
-* Parallel checking of nested Isar proofs, with improved scalability
-up to 8 cores.
+* FIXME
 
 
-You may get Isabelle2009-1 from the following mirror sites:
+You may get Isabelle2009-2 from the following mirror sites:
 
   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
   Munich (Germany)     http://isabelle.in.tum.de/
diff -r c96e119b7fe9 -r 07f3f5a03e98 COPYRIGHT
--- a/COPYRIGHT	Thu May 27 21:37:42 2010 +0200
+++ b/COPYRIGHT	Fri May 28 11:23:34 2010 +0200
@@ -1,6 +1,6 @@
 ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.
 
-Copyright (c) 2009,
+Copyright (c) 2010,
   University of Cambridge and
   Technische Universitaet Muenchen.
 
diff -r c96e119b7fe9 -r 07f3f5a03e98 README
--- a/README	Thu May 27 21:37:42 2010 +0200
+++ b/README	Fri May 28 11:23:34 2010 +0200
@@ -9,8 +9,9 @@
 
 System requirements
 
-   Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
-   following additional software:
+   Isabelle requires a regular Unix-style platform (e.g. Linux,
+   Windows with Cygwin, Mac OS) and depends on the following main
+   add-on tools:
 
      * The Poly/ML compiler and runtime system (version 5.x).
      * The GNU bash shell (version 3.x or 2.x).
@@ -20,7 +21,7 @@
 
 Installation
 
-   Binary packages are available for Isabelle/HOL and ZF for several
+   Binary packages are available for Isabelle/HOL etc. for several
    platforms from the Isabelle web page. The system may be also built
    from scratch, using the tar.gz source distribution. See file
    INSTALL as distributed with Isabelle for more information.
@@ -32,9 +33,8 @@
 
    The classic Isabelle user interface is Proof General by David
    Aspinall and others. It is a generic Emacs interface for proof
-   assistants, including Isabelle. Proof General is suitable for use
-   by pacifists and Emacs militants alike. Its most prominent feature
-   is script management, providing a metaphor of live proof script
+   assistants, including Isabelle.  Its most prominent feature is
+   script management, providing a metaphor of stepwise proof script
    editing.  Proof General also provides some support for mathematical
    symbols displayed on screen.