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