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

[Jasmin Blanchette]

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

Indeed, there's some brokenness with Skolemization which is perhaps not so hard to fix -- given that this used to work much better back in 2016, according to our JAR paper ("Semi-intelligible ..."). Esp. back then we had it working reliably for E, which is no longer the case it seems. Maybe the provers have changed their format a bit and we don't pick them up correctly. It's on our list, but I'm afraid probably not for the next release. Martin, Mathias, and I are doing all of that as a "hobby", and Makarius's offer to build the binaries relieved me from a huge weight. The situation is, thanks to them, still much better than only a few months ago.

Jasmin