Re: [isabelle] Auto sledgehammer on completed lemmas
On 04.06.2015 09:44, Gerwin Klein wrote:
> And autosolve skip those that are already solved by a single rule application with one of the rules it is suggesting. But thatâs probably a lot of proof text analysis for something that doesnât really want to know about any of that.
I'd like autosolve to skip non-lemma proof-obligations (for example
those of sublocale); at least if these have a successful proof.
This archive was generated by a fusion of
Pipermail (Mailman edition) and