[isabelle-dev] [Spam] NEWS: update of external provers

[Lawrence Paulson]

The main problem with these monsters is that they often don’t work, and related to this, they often “obtain” functions that don’t appear to be necessary. Where monsters do work, they often suggest quite relevant lemmas.
Larry

> On 20 Oct 2020, at 15:27, Jasmin Blanchette <j.c.blanchette at vu.nl> wrote:
> 
> On the positive side, veriT outputs detailed proofs (like Z3 but unlike CVC4), which are parsed by Isabelle and yield these "semi-intelligible Isar monsters". Some users find that they can fish out useful bits from them, if not use them as is; others find them too broken or ugly. Improving the situation here is high on my agenda for Sledgehammer, because it's generally the key to proof reconstruction for stronger ATPs (e.g. HO).