author | nipkow |
Fri, 04 Dec 2020 18:29:48 +0100 | |
changeset 72810 | b00ee476151b |
parent 72807 | ea189da0ff60 |
child 72811 | ef21a1de340d |
--- a/NEWS Fri Dec 04 15:16:03 2020 +0100 +++ b/NEWS Fri Dec 04 18:29:48 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