diff -r 8fd1936490bc -r 22158ebde77f NEWS
--- 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)