[isabelle-dev] NEWS: update of external provers

[Makarius]

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