1.1 --- a/ANNOUNCE	Sat Apr 14 12:36:11 2012 +0200
     1.2 +++ b/ANNOUNCE	Sat Apr 14 12:46:45 2012 +0200
     1.3 @@ -1,29 +1,15 @@
     1.4 -Subject: Announcing Isabelle2011-1
     1.5 +Subject: Announcing Isabelle2012
     1.6  To: isabelle-users@cl.cam.ac.uk
     1.7  
     1.8 -Isabelle2011-1 is now available.
     1.9 +Isabelle2012 is now available.
    1.10  
    1.11 -This version significantly improves upon Isabelle2011, see the NEWS
    1.12 +This version significantly improves upon Isabelle2011-1, see the NEWS
    1.13  file in the distribution for more details.  Some notable changes are:
    1.14  
    1.15 -* Significantly improved Isabelle/jEdit Prover IDE (PIDE).
    1.16 +* FIXME
    1.17  
    1.18 -* Improved system integration with Isabelle/Scala: YXML data encoding.
    1.19  
    1.20 -* Improved parallel performance and scalability.
    1.21 -
    1.22 -* Improved document preparation: embedded rail-road diagrams.
    1.23 -
    1.24 -* HOL tool enhancements: Quickcheck, Nitpick, Sledgehammer, SMT/Z3
    1.25 -  integration.
    1.26 -
    1.27 -* Numerous HOL library improvements: main HOL, HOLCF, HOL-Library,
    1.28 -  Multivariate_Analysis, Probability.
    1.29 -
    1.30 -* Updated and extended Isabelle/Isar reference manual.
    1.31 -
    1.32 -
    1.33 -You may get Isabelle2011-1 from the following mirror sites:
    1.34 +You may get Isabelle2012 from the following mirror sites:
    1.35  
    1.36    Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    1.37    Munich (Germany)     http://isabelle.in.tum.de/

     2.1 --- a/CONTRIBUTORS	Sat Apr 14 12:36:11 2012 +0200
     2.2 +++ b/CONTRIBUTORS	Sat Apr 14 12:46:45 2012 +0200
     2.3 @@ -3,21 +3,25 @@
     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 Isabelle2012
    2.10 +-----------------------------
    2.11  
    2.12 -* March 2012: Christian Sternagel, Japan Advanced Institute of Science and Technology
    2.13 +* March 2012: Christian Sternagel, Japan Advanced Institute of Science
    2.14 +  and Technology
    2.15    Consolidated theory of relation composition.
    2.16  
    2.17  * March 2012: Nik Sultana, University of Cambridge
    2.18    HOL/TPTP parser and import facilities.
    2.19  
    2.20 +* March 2012: Cezary Kaliszyk, University of Innsbruck and
    2.21 +  Alexander Krauss, QAware GmbH
    2.22 +  Faster and more scalable Import mechanism for HOL Light proofs.
    2.23 +
    2.24  * January 2012: Florian Haftmann, TUM, et. al.
    2.25    (Re-)Introduction of the "set" type constructor.
    2.26  
    2.27 -* March 2012: Cezary Kaliszyk, University of Innsbruck and
    2.28 -  Alexander Krauss, QAware GmbH
    2.29 -  Faster and more scalable Import mechanism for HOL Light proofs.
    2.30 +* 2011/2012: Makarius Wenzel, Université Paris-Sud / LRI
    2.31 +  Improvements of Isabelle/Scala layer and Isabelle/jEdit Prover IDE.
    2.32  
    2.33  
    2.34  Contributions to Isabelle2011-1

     3.1 --- a/COPYRIGHT	Sat Apr 14 12:36:11 2012 +0200
     3.2 +++ b/COPYRIGHT	Sat Apr 14 12:46:45 2012 +0200
     3.3 @@ -1,6 +1,6 @@
     3.4  ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.
     3.5  
     3.6 -Copyright (c) 2011,
     3.7 +Copyright (c) 2012,
     3.8    University of Cambridge,
     3.9    Technische Universitaet Muenchen,
    3.10    and contributors.

     4.1 --- a/NEWS	Sat Apr 14 12:36:11 2012 +0200
     4.2 +++ b/NEWS	Sat Apr 14 12:46:45 2012 +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 Isabelle2012 (May 2012)
    4.10 +------------------------------
    4.11  
    4.12  *** General ***
    4.13  
    4.14 @@ -95,7 +95,7 @@
    4.15    lemma "P (x::'a::foo)" and "Q (y::'a::bar)"  -- "now illegal"
    4.16  
    4.17    lemma "P (x::'a)" and "Q (y::'a::bar)"
    4.18 -    -- "now uniform 'a::bar instead of default sort for first occurence (!)"
    4.19 +    -- "now uniform 'a::bar instead of default sort for first occurrence (!)"
    4.20  
    4.21  
    4.22  *** HOL ***

     5.1 --- a/README	Sat Apr 14 12:36:11 2012 +0200
     5.2 +++ b/README	Sat Apr 14 12:46:45 2012 +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 or 1.7.x from Oracle or Apple -- for Scala and jEdit.
    5.10 +     * GNU Emacs (version 23 or 24) -- for the Proof General 4.x interface.
    5.11       * A complete LaTeX installation -- for document preparation.
    5.12  
    5.13  Installation