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.

  -- Lars




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