# HG changeset patch
# User Peter Lammich
# Date 1607104517 0
# Node ID b09f358f3eb0b94ba1d19824d70697d86b0db4cb
# Parent  caf2fd14e28b913d1982830c087e1a5072e7d634# Parent  ef21a1de340de0f426f4465ed29b5aceb2d7c75c
merged

diff -r caf2fd14e28b -r b09f358f3eb0 NEWS
--- a/NEWS	Fri Dec 04 17:54:57 2020 +0000
+++ b/NEWS	Fri Dec 04 17:55:17 2020 +0000
@@ -87,6 +87,8 @@
 
 *** 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