--- a/NEWS Tue Feb 11 15:41:40 2020 +0100
+++ b/NEWS Tue Feb 11 17:03:14 2020 +0100
@@ -97,8 +97,11 @@
* Session HOL-Analysis: proof method "metric" implements a decision
procedure for simple linear statements in metric spaces.
-* Session HOL-Word: Bitwise NOT-operator has proper prefix syntax. Minor
-INCOMPATIBILITY.
+* Session HOL-Word: bitwise NOT-operator has proper prefix syntax. Minor
+INCOMPATIBILITY.
+
+* Session HOL-Proofs: build faster thanks to better treatment of proof
+terms in Isabelle/Pure.
*** ML ***
@@ -116,6 +119,9 @@
general Proof_Context.augment: it is subject to an optional soft-type
system of the underlying object-logic. Minor INCOMPATIBILITY.
+* More scalable Export.export using XML.tree to avoid premature string
+allocations, with convenient shortcut XML.blob. Minor INCOMPATIBILITY.
+
*** System ***
@@ -147,6 +153,12 @@
splitting sessions and supporting a base logic image. Minor
INCOMPATIBILITY in options and parameters.
+* Isabelle/Scala support for the Linux platform (Ubuntu): packages,
+users, system services.
+
+* Isabelle/Scala support for proof terms (with full type/term
+information) in module isabelle.Term.
+
* Theory export via Isabelle/Scala has been reworked. The former "fact"
name space is now split into individual "thm" items: names are
potentially indexed, such as "foo" for singleton facts, or "bar(1)",
@@ -158,6 +170,13 @@
* Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM
have been discontinued -- deprecated since Isabelle2018.
+* More complete x86_64 platform support on macOS, notably Catalina where
+old x86 has been discontinued.
+
+* Update to GHC stack 2.1.3 with stackage lts-13.19/ghc-8.6.4.
+
+* Update to OCaml Opam 2.0.6 (using ocaml 4.05.0 as before).
+
New in Isabelle2019 (June 2019)