--- a/NEWS Wed Feb 26 16:08:05 2020 +0100
+++ b/NEWS Wed Feb 26 19:26:00 2020 +0100
@@ -67,7 +67,8 @@
*** Isabelle/VSCode Prover IDE ***
-* Update to WebviewPanel API.
+* Update of State and Preview panels to use new WebviewPanel API of
+VSCode.
*** HOL ***
@@ -105,14 +106,16 @@
* Theory HOL-Library.Ramsey: full finite Ramsey's theorem with
multiple colours and arbitrary exponents.
-* Session HOL-Analysis: proof method "metric" implements a decision
-procedure for simple linear statements in metric spaces.
+* Session HOL-Proofs: build faster thanks to better treatment of proof
+terms in Isabelle/Pure.
* 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.
+* Session HOL-Analysis: proof method "metric" implements a decision
+procedure for simple linear statements in metric spaces.
+
+* Session HOL-Complex_Analysis has been split off from HOL-Analysis.
*** ML ***
@@ -178,6 +181,10 @@
inferences; it might help to reconstruct the formal structure of theory
libraries. See also the module Export_Theory in Isabelle/Scala.
+* Theory export of structured specifications, based on internal
+declarations of Spec_Rules by packages like 'definition', 'inductive',
+'primrec', 'function'.
+
* Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM
have been discontinued -- deprecated since Isabelle2018.