[isabelle-dev] NEWS: update of external provers

[Lawrence Paulson]

I was wanting to know exactly the same thing. In particular, will sledgehammer suggest it now? And does it give us a version of the smt method more robust than the existing one?

Larry

> On 19 Oct 2020, at 16:39, Makarius <makarius at sketis.net> wrote:
> 
> 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.)