[isabelle] Auto sledgehammer on completed lemmas



Hi all,

I've noticed after enabling auto-Sledgehammer that it (and friends like Nitpick) run on all the
lemmas in any file you open. So, for example, when you open a previously worked on theory,
Sledgehammer starts attacking lemmas that already have completed proofs. This isn't a large
impediment, but I just wanted to suggest that perhaps this behaviour could be improved on in future
by noticing the completed proof.

If there's a way to alter this behaviour that I have overlooked, please let me know and apologies
for the noise.

Thanks,
Matt

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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