equal
deleted
inserted
replaced
84 |
84 |
85 * Local_Theory.init replaces Generic_Target.init. Minor INCOMPATIBILITY. |
85 * Local_Theory.init replaces Generic_Target.init. Minor INCOMPATIBILITY. |
86 |
86 |
87 |
87 |
88 *** HOL *** |
88 *** HOL *** |
|
89 |
|
90 * Session "Hoare" now provides a total correctness logic as well. |
89 |
91 |
90 * An updated version of the veriT solver is now included as Isabelle |
92 * An updated version of the veriT solver is now included as Isabelle |
91 component. It can be used in the "smt" proof method via "smt (verit)" or |
93 component. It can be used in the "smt" proof method via "smt (verit)" or |
92 via "declare [[smt_solver = verit]]" in the context; see also session |
94 via "declare [[smt_solver = verit]]" in the context; see also session |
93 HOL-Word-SMT_Examples. |
95 HOL-Word-SMT_Examples. |