--- a/ANNOUNCE Tue Apr 02 14:12:21 2019 +0200
+++ b/ANNOUNCE Tue Apr 02 14:46:01 2019 +0200
@@ -1,37 +1,37 @@
Subject: Announcing Isabelle2018
To: isabelle-users@cl.cam.ac.uk
-Isabelle2018 is now available.
+Isabelle2019 is now available.
-This version introduces many changes over Isabelle2017: see the NEWS
+This version introduces many changes over Isabelle2018: see the NEWS
file for further details. Here are some notable points:
-* Improved infix notation within terms.
+* Improved "Isabelle DejaVu" font collection, suitable for text and GUI.
-* Improved syntax for formal comments, within terms and other languages.
+* Various Isabelle/jEdit improvements, with virtual file-system access to
+sessions and exports.
-* Improved management of ROOT files and session-qualified theories.
+* Improved headless PIDE session (and server).
-* Various improvements of document preparation.
-
-* Many Isabelle/jEdit improvements, including semantic IDE for BibTeX.
+* HOL: 'export_code' now generates logical files in the theory and session
+context, e.g. browsable as "isabelle-export:" in Isabelle/jEdit.
-* Numerous HOL library improvements, including HOL-Algebra.
+* HOL: various syntax and library improvements.
-* Substantial additions to HOL-Analysis.
+* HOL-Analysis: more material and better organization.
-* HOL-Library.Code_Lazy: code generation for lazy evaluation.
+* Isabelle/ML environments for separate SML applications.
-* HOL-Real_Asymp: tools for semi-automatic real asymptotics.
+* Isabelle/Haskell library for implementation of Isabelle/PIDE backends.
-* Isabelle server for reactive communication with other programs.
+* Installation management for Haskell (Stack) and OCaml (OPAM).
-* More uniform 64-bit platform support: smaller Isabelle application.
+* Update to current Java 11 and Poly/ML 5.8 with better scalability.
-You may get Isabelle2018 from the following mirror sites:
+You may get Isabelle2019 from the following mirror sites:
Cambridge (UK) https://www.cl.cam.ac.uk/research/hvg/Isabelle
Munich (Germany) https://isabelle.in.tum.de
- Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle
+ Sydney (Australia) https://mirror.cse.unsw.edu.au/pub/isabelle
Potsdam, NY (USA) https://mirror.clarkson.edu/isabelle
--- a/NEWS Tue Apr 02 14:12:21 2019 +0200
+++ b/NEWS Tue Apr 02 14:46:01 2019 +0200
@@ -9,8 +9,8 @@
*** General ***
-* The font family "Isabelle DejaVu" is systematically derived from the
-existing "DejaVu" collection, with variants "Sans Mono", "Sans", "Serif"
+* The font collection "Isabelle DejaVu" is systematically derived from
+the existing "DejaVu" fonts, with variants "Sans Mono", "Sans", "Serif"
and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".
The DejaVu base fonts are retricted to well-defined Unicode ranges and
augmented by special Isabelle symbols, taken from the former
@@ -210,6 +210,8 @@
* Session HOL-Number_Theory: More material on residue rings in
Carmichael's function, primitive roots, more properties for "ord".
+* Session HOL-Analysis: More material and better organization.
+
* Session HOL-SPARK: .prv files are no longer written to the
file-system, but exported to the session database. Results may be
retrieved via "isabelle build -e HOL-SPARK-Examples" on the