updated for release;
authorwenzelm
Tue Feb 11 17:03:14 2020 +0100 (2 weeks ago)
changeset 7143822158ebde77f
parent 71437 8fd1936490bc
child 71439 760e19aa9b09
updated for release;
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Tue Feb 11 15:41:40 2020 +0100
     1.2 +++ b/CONTRIBUTORS	Tue Feb 11 17:03:14 2020 +0100
     1.3 @@ -13,16 +13,24 @@
     1.4    The full finite Ramsey's theorem and elements of finite and infinite
     1.5    Ramsey theory.
     1.6  
     1.7 -* December 2019:
     1.8 -  Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel
     1.9 +* December 2019: Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy
    1.10 +  Traytel
    1.11    Extension of lift_bnf to support quotient types.
    1.12  
    1.13 +* October..December 2019: Makarius Wenzel
    1.14 +  Isabelle/Phabrictor server setup, including Linux platform support in
    1.15 +  Isabelle/Scala. Client-side tool "isabelle hg_setup".
    1.16 +
    1.17  * October 2019: Maximilian Schäffeler
    1.18    Port of the HOL Light decision procedure for metric spaces.
    1.19  
    1.20  * October 2019: Makarius Wenzel
    1.21    More scalable Isabelle dump and underlying headless PIDE session.
    1.22  
    1.23 +* August 2019: Makarius Wenzel
    1.24 +  Better support for proof terms in Isabelle/Pure, notably via method
    1.25 +  combinator SUBPROOFS (ML) and "subproofs" (Isar).
    1.26 +
    1.27  * July 2019: Alexander Krauss, Makarius Wenzel
    1.28    Minimal support for a soft-type system within the Isabelle logical
    1.29    framework.
     2.1 --- a/NEWS	Tue Feb 11 15:41:40 2020 +0100
     2.2 +++ b/NEWS	Tue Feb 11 17:03:14 2020 +0100
     2.3 @@ -97,8 +97,11 @@
     2.4  * Session HOL-Analysis: proof method "metric" implements a decision
     2.5  procedure for simple linear statements in metric spaces.
     2.6  
     2.7 -* Session HOL-Word: Bitwise NOT-operator has proper prefix syntax. Minor
     2.8 -INCOMPATIBILITY.
     2.9 +* Session HOL-Word: bitwise NOT-operator has proper prefix syntax. Minor
    2.10 +INCOMPATIBILITY.
    2.11 +
    2.12 +* Session HOL-Proofs: build faster thanks to better treatment of proof
    2.13 +terms in Isabelle/Pure.
    2.14  
    2.15  
    2.16  *** ML ***
    2.17 @@ -116,6 +119,9 @@
    2.18  general Proof_Context.augment: it is subject to an optional soft-type
    2.19  system of the underlying object-logic. Minor INCOMPATIBILITY.
    2.20  
    2.21 +* More scalable Export.export using XML.tree to avoid premature string
    2.22 +allocations, with convenient shortcut XML.blob. Minor INCOMPATIBILITY.
    2.23 +
    2.24  
    2.25  *** System ***
    2.26  
    2.27 @@ -147,6 +153,12 @@
    2.28  splitting sessions and supporting a base logic image. Minor
    2.29  INCOMPATIBILITY in options and parameters.
    2.30  
    2.31 +* Isabelle/Scala support for the Linux platform (Ubuntu): packages,
    2.32 +users, system services.
    2.33 +
    2.34 +* Isabelle/Scala support for proof terms (with full type/term
    2.35 +information) in module isabelle.Term.
    2.36 +
    2.37  * Theory export via Isabelle/Scala has been reworked. The former "fact"
    2.38  name space is now split into individual "thm" items: names are
    2.39  potentially indexed, such as "foo" for singleton facts, or "bar(1)",
    2.40 @@ -158,6 +170,13 @@
    2.41  * Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM
    2.42  have been discontinued -- deprecated since Isabelle2018.
    2.43  
    2.44 +* More complete x86_64 platform support on macOS, notably Catalina where
    2.45 +old x86 has been discontinued.
    2.46 +
    2.47 +* Update to GHC stack 2.1.3 with stackage lts-13.19/ghc-8.6.4.
    2.48 +
    2.49 +* Update to OCaml Opam 2.0.6 (using ocaml 4.05.0 as before).
    2.50 +
    2.51  
    2.52  
    2.53  New in Isabelle2019 (June 2019)