some updates for release;
authorwenzelm
Wed Sep 07 20:49:45 2011 +0200 (2011-09-07)
changeset 44801a0459c50cfc9
parent 44800 0472f2367efb
child 44802 65c397cc44ec
some updates for release;
ANNOUNCE
Admin/CHECKLIST
CONTRIBUTORS
NEWS
README
doc/Contents
     1.1 --- a/ANNOUNCE	Wed Sep 07 20:29:54 2011 +0200
     1.2 +++ b/ANNOUNCE	Wed Sep 07 20:49:45 2011 +0200
     1.3 @@ -1,34 +1,15 @@
     1.4 -Subject: Announcing Isabelle2011
     1.5 +Subject: Announcing Isabelle2011-1
     1.6  To: isabelle-users@cl.cam.ac.uk
     1.7  
     1.8 -Isabelle2011 is now available.
     1.9 -
    1.10 -This version significantly improves upon Isabelle2009-2, see the NEWS
    1.11 -file in the distribution for more details.  Some notable changes are:
    1.12 -
    1.13 -* Experimental Prover IDE based on Isabelle/Scala and jEdit.
    1.14 -
    1.15 -* Coercive subtyping (configured in HOL/Complex_Main).
    1.16 -
    1.17 -* HOL code generation: Scala as another target language.
    1.18 -
    1.19 -* HOL: partial_function definitions.
    1.20 +Isabelle2011-1 is now available.
    1.21  
    1.22 -* HOL: various tool enhancements, including Quickcheck, Nitpick,
    1.23 -  Sledgehammer, SMT integration.
    1.24 -
    1.25 -* HOL: various additions to theory library, including HOL-Algebra,
    1.26 -  Imperative_HOL, Multivariate_Analysis, Probability.
    1.27 +This version improves upon Isabelle2011, see the NEWS file in the
    1.28 +distribution for more details.  Some important changes are:
    1.29  
    1.30 -* HOLCF: reorganization of library and related tools.
    1.31 -
    1.32 -* HOL/SPARK: interactive proof environment for verification conditions
    1.33 -  generated by the SPARK Ada program verifier.
    1.34 -
    1.35 -* Improved Isabelle/Isar implementation manual (covering Isabelle/ML).
    1.36 +* FIXME
    1.37  
    1.38  
    1.39 -You may get Isabelle2011 from the following mirror sites:
    1.40 +You may get Isabelle2011-1 from the following mirror sites:
    1.41  
    1.42    Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    1.43    Munich (Germany)     http://isabelle.in.tum.de/
     2.1 --- a/Admin/CHECKLIST	Wed Sep 07 20:29:54 2011 +0200
     2.2 +++ b/Admin/CHECKLIST	Wed Sep 07 20:49:45 2011 +0200
     2.3 @@ -3,9 +3,7 @@
     2.4  
     2.5  - test polyml-5.4.0, polyml-5.3.0, polyml-5.2.1, smlnj;
     2.6  
     2.7 -- test Proof General 4.1, 4.0, 3.7.1.1;
     2.8 -
     2.9 -- test Scala wrapper;
    2.10 +- test Proof General 4.1, 3.7.1.1;
    2.11  
    2.12  - check HTML header of library;
    2.13  
     3.1 --- a/CONTRIBUTORS	Wed Sep 07 20:29:54 2011 +0200
     3.2 +++ b/CONTRIBUTORS	Wed Sep 07 20:49:45 2011 +0200
     3.3 @@ -3,8 +3,8 @@
     3.4  who is listed as an author in one of the source files of this Isabelle
     3.5  distribution.
     3.6  
     3.7 -Contributions to this Isabelle version
     3.8 ---------------------------------------
     3.9 +Contributions to Isabelle2011-1
    3.10 +-------------------------------
    3.11  
    3.12  
    3.13  Contributions to Isabelle2011
     4.1 --- a/NEWS	Wed Sep 07 20:29:54 2011 +0200
     4.2 +++ b/NEWS	Wed Sep 07 20:49:45 2011 +0200
     4.3 @@ -1,8 +1,8 @@
     4.4  Isabelle NEWS -- history user-relevant changes
     4.5  ==============================================
     4.6  
     4.7 -New in this Isabelle version
     4.8 -----------------------------
     4.9 +New in Isabelle2011-1 (October 2011)
    4.10 +------------------------------------
    4.11  
    4.12  *** General ***
    4.13  
     5.1 --- a/README	Wed Sep 07 20:29:54 2011 +0200
     5.2 +++ b/README	Wed Sep 07 20:49:45 2011 +0200
     5.3 @@ -16,8 +16,8 @@
     5.4       * The Poly/ML compiler and runtime system (version 5.2.1 or later).
     5.5       * The GNU bash shell (version 3.x or 2.x).
     5.6       * Perl (version 5.x).
     5.7 +     * Java 1.6.x from Oracle or Apple -- for Scala and jEdit.
     5.8       * GNU Emacs (version 23) -- for the Proof General 4.x interface.
     5.9 -     * Java 1.6.x from Oracle/Sun or Apple -- for Scala and jEdit.
    5.10       * A complete LaTeX installation -- for document preparation.
    5.11  
    5.12  Installation
    5.13 @@ -31,17 +31,18 @@
    5.14  
    5.15  User interface
    5.16  
    5.17 +   Isabelle/jEdit is an emerging Prover IDE based on advanced
    5.18 +   technology of Isabelle/Scala.  It provides a metaphor of continuous
    5.19 +   proof checking of a versioned collection of theory sources, with
    5.20 +   instantaneous feedback in real-time and rich semantic markup
    5.21 +   associated with the formal text.
    5.22 +
    5.23     The classic Isabelle user interface is Proof General by David
    5.24     Aspinall and others.  It is a generic Emacs interface for proof
    5.25     assistants, including Isabelle.  Its most prominent feature is
    5.26     script management, providing a metaphor of stepwise proof script
    5.27     editing.
    5.28  
    5.29 -   Isabelle/jEdit is an experimental Prover IDE based on advanced
    5.30 -   technology of Isabelle/Scala.  It provides a metaphor of continuous
    5.31 -   proof checking of a versioned collection of theory sources, with
    5.32 -   instantaneous feedback in real-time.
    5.33 -
    5.34  Other sources of information
    5.35  
    5.36    The Isabelle Page
     6.1 --- a/doc/Contents	Wed Sep 07 20:29:54 2011 +0200
     6.2 +++ b/doc/Contents	Wed Sep 07 20:49:45 2011 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -Learning and using Isabelle
     6.5 +Miscellaneous tutorials
     6.6    tutorial        Tutorial on Isabelle/HOL
     6.7    main            What's in Main
     6.8    isar-overview   Tutorial on Isar