--- a/CONTRIBUTORS Tue Feb 11 15:41:40 2020 +0100
+++ b/CONTRIBUTORS Tue Feb 11 17:03:14 2020 +0100
@@ -13,16 +13,24 @@
The full finite Ramsey's theorem and elements of finite and infinite
Ramsey theory.
-* December 2019:
- Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel
+* December 2019: Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy
+ Traytel
Extension of lift_bnf to support quotient types.
+* October..December 2019: Makarius Wenzel
+ Isabelle/Phabrictor server setup, including Linux platform support in
+ Isabelle/Scala. Client-side tool "isabelle hg_setup".
+
* October 2019: Maximilian Schäffeler
Port of the HOL Light decision procedure for metric spaces.
* October 2019: Makarius Wenzel
More scalable Isabelle dump and underlying headless PIDE session.
+* August 2019: Makarius Wenzel
+ Better support for proof terms in Isabelle/Pure, notably via method
+ combinator SUBPROOFS (ML) and "subproofs" (Isar).
+
* July 2019: Alexander Krauss, Makarius Wenzel
Minimal support for a soft-type system within the Isabelle logical
framework.
--- 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)