misc tuning and updates for release;
authorwenzelm
Fri Jun 29 20:11:17 2018 +0200 (12 months ago)
changeset 685457922992c99ea
parent 68544 8285fa53bfac
child 68546 34d732a83767
misc tuning and updates for release;
ANNOUNCE
CONTRIBUTORS
NEWS
     1.1 --- a/ANNOUNCE	Fri Jun 29 19:53:15 2018 +0200
     1.2 +++ b/ANNOUNCE	Fri Jun 29 20:11:17 2018 +0200
     1.3 @@ -4,9 +4,25 @@
     1.4  Isabelle2018 is now available.
     1.5  
     1.6  This version introduces many changes over Isabelle2017: see the NEWS
     1.7 -file for further details. Some notable points:
     1.8 +file for further details. Here are the main points:
     1.9 +
    1.10 +* Improved infix notation within terms.
    1.11 +
    1.12 +* Improved syntax for formal comments, within terms and other languages.
    1.13 +
    1.14 +* Improved management of ROOT files and session-qualified theories.
    1.15 +
    1.16 +* Various improvements of document preparation.
    1.17  
    1.18 -* FIXME.
    1.19 +* Many Isabelle/jEdit improvements, including semantic IDE for Bibtex.
    1.20 +
    1.21 +* Numerous HOL library improvements, including HOL-Algebra.
    1.22 +
    1.23 +* Substantial additions to HOL-Analysis.
    1.24 +
    1.25 +* Isabelle server for reactive communication with other programs.
    1.26 +
    1.27 +* More uniform 64-bit platform support: smaller Isabelle application.
    1.28  
    1.29  
    1.30  You may get Isabelle2018 from the following mirror sites:
     2.1 --- a/CONTRIBUTORS	Fri Jun 29 19:53:15 2018 +0200
     2.2 +++ b/CONTRIBUTORS	Fri Jun 29 20:11:17 2018 +0200
     2.3 @@ -12,6 +12,10 @@
     2.4  * June 2018: Martin Baillon and Paulo Emílio de Vilhena
     2.5    A variety of contributions to HOL-Algebra.
     2.6  
     2.7 +* May/June 2018: Makarius Wenzel
     2.8 +  System infrastructure to export blobs as theory presentation, and to dump
     2.9 +  PIDE database content in batch mode.
    2.10 +
    2.11  * May 2018: Manuel Eberl
    2.12    Landau symbols and asymptotic equivalence (moved from the AFP).
    2.13  
     3.1 --- a/NEWS	Fri Jun 29 19:53:15 2018 +0200
     3.2 +++ b/NEWS	Fri Jun 29 20:11:17 2018 +0200
     3.3 @@ -128,14 +128,14 @@
     3.4  plain-text document draft. Both are available via the menu "Plugins /
     3.5  Isabelle".
     3.6  
     3.7 -* Bibtex database files (.bib) are semantically checked.
     3.8 -
     3.9  * When loading text files, the Isabelle symbols encoding UTF-8-Isabelle
    3.10  is only used if there is no conflict with existing Unicode sequences in
    3.11  the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle
    3.12  symbols remain in literal \<symbol> form. This avoids accidental loss of
    3.13  Unicode content when saving the file.
    3.14  
    3.15 +* Bibtex database files (.bib) are semantically checked.
    3.16 +
    3.17  * Update to jedit-5.5.0, the latest release.
    3.18  
    3.19  
    3.20 @@ -403,10 +403,9 @@
    3.21  Riemann mapping theorem, the Vitali covering theorem,
    3.22  change-of-variables results for integration and measures.
    3.23  
    3.24 -* Session HOL-Types_To_Sets: more tool support
    3.25 -(unoverload_type combines internalize_sorts and unoverload) and larger
    3.26 -experimental application (type based linear algebra transferred to linear
    3.27 -algebra on subspaces).
    3.28 +* Session HOL-Types_To_Sets: more tool support (unoverload_type combines
    3.29 +internalize_sorts and unoverload) and larger experimental application
    3.30 +(type based linear algebra transferred to linear algebra on subspaces).
    3.31  
    3.32  
    3.33  *** ML ***