diff -r d231d71d27b4 -r b1be35908165 NEWS
--- a/NEWS	Wed Dec 23 20:49:05 2020 +0100
+++ b/NEWS	Wed Dec 23 21:06:31 2020 +0100
@@ -103,8 +103,6 @@
 
 *** HOL ***
 
-* Session "Hoare" now provides a total correctness logic as well.
-
 * An updated version of the veriT solver is now included as Isabelle
 component. It can be used in the "smt" proof method via "smt (verit)" or
 via "declare [[smt_solver = verit]]" in the context; see also session
@@ -213,6 +211,11 @@
 * Syntax for reflected term syntax is organized in bundle term_syntax,
 discontinuing previous locale term_syntax.  Minor INCOMPATIBILITY.
 
+* Session "HOL-Hoare": concrete syntax only for Hoare triples, not
+abstract language constructors.
+
+* Session "HOL-Hoare": now provides a total correctness logic as well.
+
 
 *** FOL ***