merged
authorPeter Lammich
Fri, 04 Dec 2020 17:55:17 +0000
changeset 72813 b09f358f3eb0
parent 72812 caf2fd14e28b (current diff)
parent 72811 ef21a1de340d (diff)
child 72828 18bc50e58e38
merged
--- 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