tuned;
authorwenzelm
Thu, 03 Oct 2013 16:09:47 +0200
changeset 54051 cdba71c67860
parent 54050 48c800d8ba2d
child 54052 797ae756d64d
tuned;
ANNOUNCE
CONTRIBUTORS
README
--- 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