author | wenzelm |

Sun Jan 20 14:00:05 2013 +0100 (2013-01-20) | |

changeset 50991 | b3c6c9ef11b8 |

parent 50990 | 11996ea98bbe |

child 50992 | c633700b2d9f |

misc tuning for release;

ANNOUNCE | file | annotate | diff | revisions | |

CONTRIBUTORS | file | annotate | diff | revisions | |

NEWS | file | annotate | diff | revisions |

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