misc updates for release;
authorwenzelm
Thu Dec 31 21:06:09 2015 +0100 (2015-12-31)
changeset 62016740c70a21523
parent 62015 db9c2af6ce72
child 62017 038ee85c95e4
misc updates for release;
ANNOUNCE
CONTRIBUTORS
COPYRIGHT
NEWS
     1.1 --- a/ANNOUNCE	Thu Dec 31 20:57:00 2015 +0100
     1.2 +++ b/ANNOUNCE	Thu Dec 31 21:06:09 2015 +0100
     1.3 @@ -1,36 +1,16 @@
     1.4 -Subject: Announcing Isabelle2015
     1.5 +Subject: Announcing Isabelle2016
     1.6  To: isabelle-users@cl.cam.ac.uk
     1.7  
     1.8 -Isabelle2015 is now available.
     1.9 +Isabelle2016 is now available.
    1.10  
    1.11 -This version improves upon Isabelle2014 in many ways, see the NEWS file in
    1.12 -the distribution for more details. Some important points are as follows.
    1.13 +This version improves upon Isabelle2015 in numerous ways, see the NEWS
    1.14 +file in the distribution for further details. Some highlights are as
    1.15 +follows.
    1.16  
    1.17 -* Improved Isabelle/jEdit Prover IDE: folding / bracket matching for Isar,
    1.18 -support for BibTeX files, improved graphview panel, improved scheduling for
    1.19 -asynchronous print commands (e.g. Sledgehammer provers).
    1.20 +* FIXME
    1.21  
    1.22 -* Support for 'private' and 'qualified' name space modifiers.
    1.23  
    1.24 -* Structural composition of proof methods (meth1; meth2) in Isar.
    1.25 -
    1.26 -* HOL: BNF datatypes and codatatypes are now standard.
    1.27 -
    1.28 -* HOL: numerous tool improvements: Nitpick, Sledgehammer, SMT, including a
    1.29 -new free (!) version of Z3.
    1.30 -
    1.31 -* HOL: numerous library refinements and enhancements.
    1.32 -
    1.33 -* New proof method "rewrite" for single-step rewriting with subterm
    1.34 -selection based on patterns.
    1.35 -
    1.36 -* New Eisbach proof method language and "match" method.
    1.37 -
    1.38 -* Updated manuals: datatypes, implementation, isar-ref, jedit, sledgehammer,
    1.39 -system.
    1.40 -
    1.41 -
    1.42 -You may get Isabelle2015 from the following mirror sites:
    1.43 +You may get Isabelle2016 from the following mirror sites:
    1.44  
    1.45    Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    1.46    Munich (Germany)     http://isabelle.in.tum.de/
     2.1 --- a/CONTRIBUTORS	Thu Dec 31 20:57:00 2015 +0100
     2.2 +++ b/CONTRIBUTORS	Thu Dec 31 21:06:09 2015 +0100
     2.3 @@ -3,12 +3,12 @@
     2.4  who is listed as an author in one of the source files of this Isabelle
     2.5  distribution.
     2.6  
     2.7 -Contributions to this Isabelle version
     2.8 ---------------------------------------
     2.9 +Contributions to Isabelle2016
    2.10 +-----------------------------
    2.11  
    2.12  * Autumn 2015: Florian Haftmann, TUM
    2.13 -  Rewrite definitions for global interpretations and
    2.14 -  sublocale declarations.
    2.15 +  Rewrite definitions for global interpretations and sublocale
    2.16 +  declarations.
    2.17  
    2.18  * Autumn 2015: Andreas Lochbihler
    2.19    Bourbaki-Witt fixpoint theorem for increasing functions on
     3.1 --- a/COPYRIGHT	Thu Dec 31 20:57:00 2015 +0100
     3.2 +++ b/COPYRIGHT	Thu Dec 31 21:06:09 2015 +0100
     3.3 @@ -1,6 +1,6 @@
     3.4  ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.
     3.5  
     3.6 -Copyright (c) 1986-2015,
     3.7 +Copyright (c) 1986-2016,
     3.8    University of Cambridge,
     3.9    Technische Universitaet Muenchen,
    3.10    and contributors.
     4.1 --- a/NEWS	Thu Dec 31 20:57:00 2015 +0100
     4.2 +++ b/NEWS	Thu Dec 31 21:06:09 2015 +0100
     4.3 @@ -4,8 +4,8 @@
     4.4  (Note: Isabelle/jEdit shows a tree-view of this file in Sidekick.)
     4.5  
     4.6  
     4.7 -New in this Isabelle version
     4.8 -----------------------------
     4.9 +New in Isabelle2016 (February 2015)
    4.10 +-----------------------------------
    4.11  
    4.12  *** General ***
    4.13