author | nipkow |
Fri, 04 Dec 2020 18:30:00 +0100 | |
changeset 72811 | ef21a1de340d |
parent 72809 | 64d8a7e6d8fa (current diff) |
parent 72810 | b00ee476151b (diff) |
child 72813 | b09f358f3eb0 |
--- a/NEWS Fri Dec 04 17:21:09 2020 +0000 +++ b/NEWS Fri Dec 04 18:30:00 2020 +0100 @@ -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