misc tuning for release;
authorwenzelm
Sun Jan 20 14:00:05 2013 +0100 (2013-01-20)
changeset 50991b3c6c9ef11b8
parent 50990 11996ea98bbe
child 50992 c633700b2d9f
misc tuning for release;
ANNOUNCE
CONTRIBUTORS
NEWS
     1.1 --- a/ANNOUNCE	Sun Jan 20 13:59:13 2013 +0100
     1.2 +++ b/ANNOUNCE	Sun Jan 20 14:00:05 2013 +0100
     1.3 @@ -1,40 +1,16 @@
     1.4 -Subject: Announcing Isabelle2012
     1.5 +Subject: Announcing Isabelle2013
     1.6  To: isabelle-users@cl.cam.ac.uk
     1.7  
     1.8 -Isabelle2012 is now available.
     1.9 -
    1.10 -This version introduces many changes and improvements over
    1.11 -Isabelle2011-1, see the NEWS file in the distribution for more
    1.12 -details.  Some highlights are:
    1.13 -
    1.14 -* Improved Isabelle/jEdit Prover IDE (PIDE).
    1.15 -
    1.16 -* Support for block-structured specification contexts.
    1.17 -
    1.18 -* Discontinued old code generator.
    1.19 -
    1.20 -* Updated manuals: prog-prove, isar-ref, implementation, system.
    1.21 -
    1.22 -* HOL: type 'a set is proper type constructor again.
    1.23 +Isabelle2013 is now available.
    1.24  
    1.25 -* HOL: improved representation of numerals.
    1.26 -
    1.27 -* HOL: new transfer and lifting packages, improved quotient package.
    1.28 -
    1.29 -* HOL tool enhancements: Quickcheck, Nitpick, Sledgehammer.
    1.30 -
    1.31 -* HOL library enhancements, including HOL-Library and HOL-Probability.
    1.32 +This version consolidates Isabelle2012 and introduces numerous
    1.33 +improvements, see the NEWS file in the distribution for more details.
    1.34 +Some highlights are:
    1.35  
    1.36 -* HOL: more TPTP support.
    1.37 -
    1.38 -* Re-implementation of HOL-Import for HOL-Light.
    1.39 -
    1.40 -* ZF: some modernization of notation and proofs.
    1.41 -
    1.42 -* System integration: improved support of Windows platform.
    1.43 +* FIXME
    1.44  
    1.45  
    1.46 -You may get Isabelle2012 from the following mirror sites:
    1.47 +You may get Isabelle2013 from the following mirror sites:
    1.48  
    1.49    Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    1.50    Munich (Germany)     http://isabelle.in.tum.de/
     2.1 --- a/CONTRIBUTORS	Sun Jan 20 13:59:13 2013 +0100
     2.2 +++ b/CONTRIBUTORS	Sun Jan 20 14:00:05 2013 +0100
     2.3 @@ -18,7 +18,7 @@
     2.4    including a smart type annotation algorithm and proof shrinking.
     2.5  
     2.6  * December 2012: Alessandro Coglio, Kestrel
     2.7 -  Contributions to HOL's Lattice library
     2.8 +  Contributions to HOL's Lattice library.
     2.9  
    2.10  * November 2012: Fabian Immler, TUM
    2.11    "Symbols" dockable for Isabelle/jEdit.
     3.1 --- a/NEWS	Sun Jan 20 13:59:13 2013 +0100
     3.2 +++ b/NEWS	Sun Jan 20 14:00:05 2013 +0100
     3.3 @@ -379,7 +379,7 @@
     3.4  with support for mixed, nested recursion and interesting non-free
     3.5  datatypes.
     3.6  
     3.7 -* HOL/Finite_Set and Relation: added new set and relation operations 
     3.8 +* HOL/Finite_Set and Relation: added new set and relation operations
     3.9  expressed by Finite_Set.fold.
    3.10  
    3.11  * New theory HOL/Library/RBT_Set: implementation of sets by red-black