# HG changeset patch # User wenzelm # Date 1380809387 -7200 # Node ID cdba71c67860cde481fce1eab3b14a1fecc57b4a # Parent 48c800d8ba2d124006da9ff29635307925666529 tuned; diff -r 48c800d8ba2d -r cdba71c67860 ANNOUNCE --- a/ANNOUNCE Thu Oct 03 12:34:32 2013 +0200 +++ b/ANNOUNCE Thu Oct 03 16:09:47 2013 +0200 @@ -7,20 +7,21 @@ improvements, see the NEWS file in the distribution for more details. Some highlights are: -* Improved Isabelle/jEdit Prover IDE. +* Significantly improved Isabelle/jEdit Prover IDE. * Consolidated multi-platform support: Linux, Windows, Mac OS X. -* New and updated manuals: datatypes, isar-ref, implementation, jedit. +* Added and updated manuals: datatypes, implementation, isar-ref, jedit. -* New Spec_Check: Quickcheck tool for Isabelle/ML. +* New Spec_Check tool: Quickcheck for Isabelle/ML. + +* HOL library enhancements: Complex_Main, HOL-Library, + HOL-Multivariate_Analysis. * HOL tool enhancements: Codegenerator, Function, Lifting, Transfer, Nitpick, Sledgehammer, -* HOL library enhancements: HOL-Library, HOL-Multivariate_Analysis. - -* HOL: improved BNF-based (co)datatype package. +* HOL-BNF: significantly improved BNF-based (co)datatype package. You may get Isabelle2013-1 from the following mirror sites: diff -r 48c800d8ba2d -r cdba71c67860 CONTRIBUTORS --- a/CONTRIBUTORS Thu Oct 03 12:34:32 2013 +0200 +++ b/CONTRIBUTORS Thu Oct 03 16:09:47 2013 +0200 @@ -19,6 +19,10 @@ Generation of elimination rules in the function package. New command "fun_cases". +* Summer 2013: Christian Sternagel, JAIST + Improved support for ad hoc overloading of constants, including + documentation and examples. + * Spring and Summer 2013: Lorenz Panny, Dmitriy Traytel, and Jasmin Blanchette, TUM Various improvements to BNF-based (co)datatype package, including @@ -29,7 +33,7 @@ * Spring 2013: Brian Huffman, Galois Inc. Improvements of the Transfer package. - + * Summer 2013: Daniel Kühlwein, ICIS, Radboud University Nijmegen Jasmin Blanchette, TUM Various improvements to MaSh, including a server mode. @@ -37,10 +41,6 @@ * First half of 2013: Steffen Smolka, TUM Further improvements to Sledgehammer's Isar proof generator. -* Summer 2013: Christian Sternagel, JAIST - Improved support for ad hoc overloading of constants, including - documentation and examples. - * May 2013: Florian Haftmann, TUM Ephemeral interpretation in local theories. diff -r 48c800d8ba2d -r cdba71c67860 README --- a/README Thu Oct 03 12:34:32 2013 +0200 +++ b/README Thu Oct 03 16:09:47 2013 +0200 @@ -14,8 +14,8 @@ include sources, documentation, and add-on tools for all supported platforms. - Some background information may be found in the Isabelle System - Manual (directory doc). + Some technical background information may be found in the Isabelle + System Manual (directory doc). User interfaces