--- 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/
--- 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;
--- 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
--- 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 ***
--- 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
--- 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