[isabelle-dev] NEWS: update of external provers

Lawrence Paulson lp15 at cam.ac.uk
Mon Oct 19 17:50:15 CEST 2020

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?


> 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.)

More information about the isabelle-dev mailing list