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