--- 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/
--- 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.
--- 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.