--- 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:
--- 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.
--- 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