--- a/ANNOUNCE Thu Dec 31 20:57:00 2015 +0100
+++ b/ANNOUNCE Thu Dec 31 21:06:09 2015 +0100
@@ -1,36 +1,16 @@
-Subject: Announcing Isabelle2015
+Subject: Announcing Isabelle2016
To: isabelle-users@cl.cam.ac.uk
-Isabelle2015 is now available.
-
-This version improves upon Isabelle2014 in many ways, see the NEWS file in
-the distribution for more details. Some important points are as follows.
-
-* Improved Isabelle/jEdit Prover IDE: folding / bracket matching for Isar,
-support for BibTeX files, improved graphview panel, improved scheduling for
-asynchronous print commands (e.g. Sledgehammer provers).
-
-* Support for 'private' and 'qualified' name space modifiers.
-
-* Structural composition of proof methods (meth1; meth2) in Isar.
+Isabelle2016 is now available.
-* HOL: BNF datatypes and codatatypes are now standard.
-
-* HOL: numerous tool improvements: Nitpick, Sledgehammer, SMT, including a
-new free (!) version of Z3.
-
-* HOL: numerous library refinements and enhancements.
+This version improves upon Isabelle2015 in numerous ways, see the NEWS
+file in the distribution for further details. Some highlights are as
+follows.
-* New proof method "rewrite" for single-step rewriting with subterm
-selection based on patterns.
-
-* New Eisbach proof method language and "match" method.
-
-* Updated manuals: datatypes, implementation, isar-ref, jedit, sledgehammer,
-system.
+* FIXME
-You may get Isabelle2015 from the following mirror sites:
+You may get Isabelle2016 from the following mirror sites:
Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/
Munich (Germany) http://isabelle.in.tum.de/
--- a/CONTRIBUTORS Thu Dec 31 20:57:00 2015 +0100
+++ b/CONTRIBUTORS Thu Dec 31 21:06:09 2015 +0100
@@ -3,12 +3,12 @@
who is listed as an author in one of the source files of this Isabelle
distribution.
-Contributions to this Isabelle version
---------------------------------------
+Contributions to Isabelle2016
+-----------------------------
* Autumn 2015: Florian Haftmann, TUM
- Rewrite definitions for global interpretations and
- sublocale declarations.
+ Rewrite definitions for global interpretations and sublocale
+ declarations.
* Autumn 2015: Andreas Lochbihler
Bourbaki-Witt fixpoint theorem for increasing functions on
--- a/COPYRIGHT Thu Dec 31 20:57:00 2015 +0100
+++ b/COPYRIGHT Thu Dec 31 21:06:09 2015 +0100
@@ -1,6 +1,6 @@
ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.
-Copyright (c) 1986-2015,
+Copyright (c) 1986-2016,
University of Cambridge,
Technische Universitaet Muenchen,
and contributors.
--- a/NEWS Thu Dec 31 20:57:00 2015 +0100
+++ b/NEWS Thu Dec 31 21:06:09 2015 +0100
@@ -4,8 +4,8 @@
(Note: Isabelle/jEdit shows a tree-view of this file in Sidekick.)
-New in this Isabelle version
-----------------------------
+New in Isabelle2016 (February 2015)
+-----------------------------------
*** General ***