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 <[email protected]> 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.) _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
