misc tuning and updates for release;

--- a/ANNOUNCE	Fri Jun 29 19:53:15 2018 +0200
+++ b/ANNOUNCE	Fri Jun 29 20:11:17 2018 +0200
@@ -4,9 +4,25 @@
 Isabelle2018 is now available.
 
 This version introduces many changes over Isabelle2017: see the NEWS
-file for further details. Some notable points:
+file for further details. Here are the main points:
+
+* Improved infix notation within terms.
+
+* Improved syntax for formal comments, within terms and other languages.
+
+* Improved management of ROOT files and session-qualified theories.
+
+* Various improvements of document preparation.
 
-* FIXME.
+* Many Isabelle/jEdit improvements, including semantic IDE for Bibtex.
+
+* Numerous HOL library improvements, including HOL-Algebra.
+
+* Substantial additions to HOL-Analysis.
+
+* Isabelle server for reactive communication with other programs.
+
+* More uniform 64-bit platform support: smaller Isabelle application.
 
 
 You may get Isabelle2018 from the following mirror sites:

--- a/CONTRIBUTORS	Fri Jun 29 19:53:15 2018 +0200
+++ b/CONTRIBUTORS	Fri Jun 29 20:11:17 2018 +0200
@@ -12,6 +12,10 @@
 * June 2018: Martin Baillon and Paulo Emílio de Vilhena
   A variety of contributions to HOL-Algebra.
 
+* May/June 2018: Makarius Wenzel
+  System infrastructure to export blobs as theory presentation, and to dump
+  PIDE database content in batch mode.
+
 * May 2018: Manuel Eberl
   Landau symbols and asymptotic equivalence (moved from the AFP).
 

--- a/NEWS	Fri Jun 29 19:53:15 2018 +0200
+++ b/NEWS	Fri Jun 29 20:11:17 2018 +0200
@@ -128,14 +128,14 @@
 plain-text document draft. Both are available via the menu "Plugins /
 Isabelle".
 
-* Bibtex database files (.bib) are semantically checked.
-
 * When loading text files, the Isabelle symbols encoding UTF-8-Isabelle
 is only used if there is no conflict with existing Unicode sequences in
 the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle
 symbols remain in literal \<symbol> form. This avoids accidental loss of
 Unicode content when saving the file.
 
+* Bibtex database files (.bib) are semantically checked.
+
 * Update to jedit-5.5.0, the latest release.
 
 
@@ -403,10 +403,9 @@
 Riemann mapping theorem, the Vitali covering theorem,
 change-of-variables results for integration and measures.
 
-* Session HOL-Types_To_Sets: more tool support
-(unoverload_type combines internalize_sorts and unoverload) and larger
-experimental application (type based linear algebra transferred to linear
-algebra on subspaces).
+* Session HOL-Types_To_Sets: more tool support (unoverload_type combines
+internalize_sorts and unoverload) and larger experimental application
+(type based linear algebra transferred to linear algebra on subspaces).
 
 
 *** ML ***