some updates for release;
authorwenzelm
Fri May 28 11:23:34 2010 +0200 (2010-05-28)
changeset 3715907f3f5a03e98
parent 37158 c96e119b7fe9
child 37160 d92638c7c38f
child 37168 5610d9097cae
some updates for release;
ANNOUNCE
COPYRIGHT
README
     1.1 --- a/ANNOUNCE	Thu May 27 21:37:42 2010 +0200
     1.2 +++ b/ANNOUNCE	Fri May 28 11:23:34 2010 +0200
     1.3 @@ -1,48 +1,16 @@
     1.4 -Subject: Announcing Isabelle2009-1
     1.5 +Subject: Announcing Isabelle2009-2
     1.6  To: isabelle-users@cl.cam.ac.uk
     1.7  
     1.8 -Isabelle2009-1 is now available.
     1.9 +Isabelle2009-2 is now available.
    1.10  
    1.11 -This release improves upon Isabelle2009 in many ways, see the NEWS
    1.12 -file in the distribution for more details.  Some important changes
    1.13 +This release improves upon Isabelle2009-1 in many respects, see the
    1.14 +NEWS file in the distribution for more details.  Some notable changes
    1.15  are:
    1.16  
    1.17 -* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
    1.18 -on a given logic image.
    1.19 -
    1.20 -* HOL-SMT: proof method "smt" for a combination of first-order logic
    1.21 -with equality, linear and nonlinear (natural/integer/real) arithmetic,
    1.22 -and fixed-size bitvectors.
    1.23 -
    1.24 -* HOL-Boogie: an interactive prover back-end for Boogie and VCC.
    1.25 -
    1.26 -* HOL: counterexample generator tool Nitpick based on the Kodkod
    1.27 -relational model finder.
    1.28 -
    1.29 -* HOL: predicate compiler turning inductive into (executable)
    1.30 -equational specifications.
    1.31 -
    1.32 -* HOL: refined number theory.
    1.33 -
    1.34 -* HOL: various parts of multivariate analysis.
    1.35 -
    1.36 -* HOL-Library: proof method "sos" (sum of squares) for nonlinear real
    1.37 -arithmetic, based on external semidefinite programming solvers.
    1.38 -
    1.39 -* HOLCF: new definitional domain package.
    1.40 -
    1.41 -* Revised tutorial on locales.
    1.42 -
    1.43 -* ML: tacticals for subgoal focus.
    1.44 -
    1.45 -* ML: support for Poly/ML 5.3.0, with improved reporting of compiler
    1.46 -errors and run-time exceptions, including detailed source positions.
    1.47 -
    1.48 -* Parallel checking of nested Isar proofs, with improved scalability
    1.49 -up to 8 cores.
    1.50 +* FIXME
    1.51  
    1.52  
    1.53 -You may get Isabelle2009-1 from the following mirror sites:
    1.54 +You may get Isabelle2009-2 from the following mirror sites:
    1.55  
    1.56    Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    1.57    Munich (Germany)     http://isabelle.in.tum.de/
     2.1 --- a/COPYRIGHT	Thu May 27 21:37:42 2010 +0200
     2.2 +++ b/COPYRIGHT	Fri May 28 11:23:34 2010 +0200
     2.3 @@ -1,6 +1,6 @@
     2.4  ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.
     2.5  
     2.6 -Copyright (c) 2009,
     2.7 +Copyright (c) 2010,
     2.8    University of Cambridge and
     2.9    Technische Universitaet Muenchen.
    2.10  
     3.1 --- a/README	Thu May 27 21:37:42 2010 +0200
     3.2 +++ b/README	Fri May 28 11:23:34 2010 +0200
     3.3 @@ -9,8 +9,9 @@
     3.4  
     3.5  System requirements
     3.6  
     3.7 -   Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
     3.8 -   following additional software:
     3.9 +   Isabelle requires a regular Unix-style platform (e.g. Linux,
    3.10 +   Windows with Cygwin, Mac OS) and depends on the following main
    3.11 +   add-on tools:
    3.12  
    3.13       * The Poly/ML compiler and runtime system (version 5.x).
    3.14       * The GNU bash shell (version 3.x or 2.x).
    3.15 @@ -20,7 +21,7 @@
    3.16  
    3.17  Installation
    3.18  
    3.19 -   Binary packages are available for Isabelle/HOL and ZF for several
    3.20 +   Binary packages are available for Isabelle/HOL etc. for several
    3.21     platforms from the Isabelle web page. The system may be also built
    3.22     from scratch, using the tar.gz source distribution. See file
    3.23     INSTALL as distributed with Isabelle for more information.
    3.24 @@ -32,9 +33,8 @@
    3.25  
    3.26     The classic Isabelle user interface is Proof General by David
    3.27     Aspinall and others. It is a generic Emacs interface for proof
    3.28 -   assistants, including Isabelle. Proof General is suitable for use
    3.29 -   by pacifists and Emacs militants alike. Its most prominent feature
    3.30 -   is script management, providing a metaphor of live proof script
    3.31 +   assistants, including Isabelle.  Its most prominent feature is
    3.32 +   script management, providing a metaphor of stepwise proof script
    3.33     editing.  Proof General also provides some support for mathematical
    3.34     symbols displayed on screen.
    3.35