--- a/NEWS Mon Feb 10 21:12:52 2020 +0100
+++ b/NEWS Mon Feb 10 21:59:24 2020 +0100
@@ -83,15 +83,15 @@
sign_simps and field_split_simps can be used instead of divide_simps.
INCOMPATIBILITY.
+* Theory HOL.Complete_Lattices:
+renamed Inf_Sup -> Inf_eq_Sup and Sup_Inf -> Sup_eq_Inf
+
* Theory HOL-Library.Monad_Syntax: infix operation "bind" (>>=)
associates to the left now as is customary.
* Theory HOL-Library.Ramsey: full finite Ramsey's theorem with
multiple colours and arbitrary exponents.
-* Theory Complete_Lattices:
-renamed Inf_Sup -> Inf_eq_Sup and Sup_Inf -> Sup_eq_Inf
-
* Session HOL-Analysis: proof method "metric" implements a decision
procedure for simple linear statements in metric spaces.
@@ -114,9 +114,6 @@
project configuration for Isabelle/Scala/jEdit, to support Scala IDEs
such as IntelliJ IDEA.
-* Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM
-have been discontinued -- deprecated since Isabelle2018.
-
* The command-line tool "isabelle phabricator_setup" facilitates
self-hosting of the Phabricator software-development platform, with
support for Git, Mercurial, Subversion repositories. This helps to avoid
@@ -142,6 +139,9 @@
inferences; it might help to reconstruct the formal structure of theory
libraries. See also the module Export_Theory in Isabelle/Scala.
+* Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM
+have been discontinued -- deprecated since Isabelle2018.
+
New in Isabelle2019 (June 2019)