On 19/10/2020 17:34, Makarius wrote:
> *** HOL ***
>
> * 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
> HOL-Word-SMT_Examples.
>
>
> *** System ***
>
> * Update/rebuild external provers on currently supported OS platforms,
> notably E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
Meta question: should we advertize these prover changes/updates more
prominently? What are really the NEWS for end-users? Is there anything in
particular to say about the brand-new "verit" vs. the old "z3"?
(The z3 component unlikely to be updated for the Isabelle2021 release, unless
Sascha Boehme finishes his long-standing effort to follow the z3 release cycle
again.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
