Re: [isabelle] sledgehammer, smt and metis

Hi Marco,

Am 21.11.2014 um 22:12 schrieb marco caminati <marco.caminati at>:

> The specific combinations usually take less then a second once I manually enter them, hence I think it's the second case.
> Given that, I find that it would be nice if sledgehammer would try those combinations, too.
> Of course I have no clue about whether this is technically possible.

It's technically possible but would put more of a burden on the user's patience. All in all, it's a matter of calibration, of trade-offs. The state you described is clearly suboptimal, but things have changed a lot in the past year or so.

So once you've upgraded to the repository version or the forthcoming Isabelle2015, keep an eye on proof reconstruction, and if you still feel things could be improved further, I would be happy to get your feedback. I have myself started using Isabelle and Sledgehammer (as opposed to developing it) and did notice a number of misfeatures, which I quickly resolved. I will still not claim that everything is perfect. ;)

> Yes, indeed a couple of Isar proofs generated by SH were readable, and I happily used them.
> It was a very nice sensation, by the way :)
> I mean, reading a proof that nobody wrote.

Thanks for the feedback!!



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.