# HG changeset patch
# User wenzelm
# Date 1315421385 -7200
# Node ID a0459c50cfc9cc10d3a8058c5115fac5b0a9e0ab
# Parent  0472f2367efb86a15d6fab44288d4e0d26834bd7
some updates for release;

diff -r 0472f2367efb -r a0459c50cfc9 ANNOUNCE
--- a/ANNOUNCE	Wed Sep 07 20:29:54 2011 +0200
+++ b/ANNOUNCE	Wed Sep 07 20:49:45 2011 +0200
@@ -1,34 +1,15 @@
-Subject: Announcing Isabelle2011
+Subject: Announcing Isabelle2011-1
 To: isabelle-users@cl.cam.ac.uk
 
-Isabelle2011 is now available.
-
-This version significantly improves upon Isabelle2009-2, see the NEWS
-file in the distribution for more details.  Some notable changes are:
-
-* Experimental Prover IDE based on Isabelle/Scala and jEdit.
-
-* Coercive subtyping (configured in HOL/Complex_Main).
-
-* HOL code generation: Scala as another target language.
-
-* HOL: partial_function definitions.
+Isabelle2011-1 is now available.
 
-* HOL: various tool enhancements, including Quickcheck, Nitpick,
-  Sledgehammer, SMT integration.
-
-* HOL: various additions to theory library, including HOL-Algebra,
-  Imperative_HOL, Multivariate_Analysis, Probability.
+This version improves upon Isabelle2011, see the NEWS file in the
+distribution for more details.  Some important changes are:
 
-* HOLCF: reorganization of library and related tools.
-
-* HOL/SPARK: interactive proof environment for verification conditions
-  generated by the SPARK Ada program verifier.
-
-* Improved Isabelle/Isar implementation manual (covering Isabelle/ML).
+* FIXME
 
 
-You may get Isabelle2011 from the following mirror sites:
+You may get Isabelle2011-1 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 0472f2367efb -r a0459c50cfc9 Admin/CHECKLIST
--- a/Admin/CHECKLIST	Wed Sep 07 20:29:54 2011 +0200
+++ b/Admin/CHECKLIST	Wed Sep 07 20:49:45 2011 +0200
@@ -3,9 +3,7 @@
 
 - test polyml-5.4.0, polyml-5.3.0, polyml-5.2.1, smlnj;
 
-- test Proof General 4.1, 4.0, 3.7.1.1;
-
-- test Scala wrapper;
+- test Proof General 4.1, 3.7.1.1;
 
 - check HTML header of library;
 
diff -r 0472f2367efb -r a0459c50cfc9 CONTRIBUTORS
--- a/CONTRIBUTORS	Wed Sep 07 20:29:54 2011 +0200
+++ b/CONTRIBUTORS	Wed Sep 07 20:49:45 2011 +0200
@@ -3,8 +3,8 @@
 who is listed as an author in one of the source files of this Isabelle
 distribution.
 
-Contributions to this Isabelle version
---------------------------------------
+Contributions to Isabelle2011-1
+-------------------------------
 
 
 Contributions to Isabelle2011
diff -r 0472f2367efb -r a0459c50cfc9 NEWS
--- a/NEWS	Wed Sep 07 20:29:54 2011 +0200
+++ b/NEWS	Wed Sep 07 20:49:45 2011 +0200
@@ -1,8 +1,8 @@
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
-New in this Isabelle version
-----------------------------
+New in Isabelle2011-1 (October 2011)
+------------------------------------
 
 *** General ***
 
diff -r 0472f2367efb -r a0459c50cfc9 README
--- a/README	Wed Sep 07 20:29:54 2011 +0200
+++ b/README	Wed Sep 07 20:49:45 2011 +0200
@@ -16,8 +16,8 @@
      * The Poly/ML compiler and runtime system (version 5.2.1 or later).
      * The GNU bash shell (version 3.x or 2.x).
      * Perl (version 5.x).
+     * Java 1.6.x from Oracle or Apple -- for Scala and jEdit.
      * GNU Emacs (version 23) -- for the Proof General 4.x interface.
-     * Java 1.6.x from Oracle/Sun or Apple -- for Scala and jEdit.
      * A complete LaTeX installation -- for document preparation.
 
 Installation
@@ -31,17 +31,18 @@
 
 User interface
 
+   Isabelle/jEdit is an emerging Prover IDE based on advanced
+   technology of Isabelle/Scala.  It provides a metaphor of continuous
+   proof checking of a versioned collection of theory sources, with
+   instantaneous feedback in real-time and rich semantic markup
+   associated with the formal text.
+
    The classic Isabelle user interface is Proof General by David
    Aspinall and others.  It is a generic Emacs interface for proof
    assistants, including Isabelle.  Its most prominent feature is
    script management, providing a metaphor of stepwise proof script
    editing.
 
-   Isabelle/jEdit is an experimental Prover IDE based on advanced
-   technology of Isabelle/Scala.  It provides a metaphor of continuous
-   proof checking of a versioned collection of theory sources, with
-   instantaneous feedback in real-time.
-
 Other sources of information
 
   The Isabelle Page
diff -r 0472f2367efb -r a0459c50cfc9 doc/Contents
--- a/doc/Contents	Wed Sep 07 20:29:54 2011 +0200
+++ b/doc/Contents	Wed Sep 07 20:49:45 2011 +0200
@@ -1,4 +1,4 @@
-Learning and using Isabelle
+Miscellaneous tutorials
   tutorial        Tutorial on Isabelle/HOL
   main            What's in Main
   isar-overview   Tutorial on Isar