diff -r f08cf9d8f90b -r 0408f6814224 NEWS
--- a/NEWS	Wed May 27 13:22:17 2020 +0200
+++ b/NEWS	Wed May 27 13:57:13 2020 +0200
@@ -7,6 +7,31 @@
 New in this Isabelle version
 ----------------------------
 
+*** Pure ***
+
+* Definitions in locales produce rule which can be added as congruence
+rule to protect foundational terms during simplification.
+
+
+*** HOL ***
+
+* Simproc "datatype_no_proper_subterm" rewrites equalities "lhs = rhs"
+on datatypes to "False" if either side is a proper subexpression of the
+other (for any datatype with a reasonable size function).
+
+* New constant "power_int" for exponentiation with integer exponent,
+written as "x powi n".
+
+* Added the "at most 1" quantifier, Uniq.
+
+* For the natural numbers, Sup{} = 0.
+
+
+*** FOL ***
+
+* Added the "at most 1" quantifier, Uniq, as in HOL.
+
+
 *** System ***
 
 * The command-line tool "isabelle console" now supports interrupts
@@ -34,23 +59,6 @@
 directory (e.g. /var/www/phabricator-vcs/libphutil).
 
 
-*** Pure ***
-
-* Definitions in locales produce rule which can be added as congruence
-rule to protect foundational terms during simplification.
-
-*** HOL ***
-
-* New constant "power_int" for exponentiation with integer exponent,
-written as "x powi n".
-
-* Added the "at most 1" quantifier, Uniq.
-
-* For the natural numbers, Sup{} = 0.
-
-*** FOL ***
-
-* Added the "at most 1" quantifier, Uniq, as in HOL.
 
 New in Isabelle2020 (April 2020)
 --------------------------------
@@ -464,10 +472,6 @@
 
 *** HOL ***
 
-* Simproc 'datatype_no_proper_subterm' rewrites equalities 'lhs = rhs'
-on datatypes to 'False' if either side is a proper subexpression of the
-other (for any datatype with a reasonable size function).
-
 * Command 'export_code' produces output as logical files within the
 theory context, as well as formal session exports that can be
 materialized via command-line tools "isabelle export" or "isabelle build