Email Gateway (Mar 29 2023 at 09:57): Email Gateway (Mar 29 2023 at 09:57):From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
In some not too distant past, Jasmin Blanchette wrote:
Indeed. There was a time where this option was new and experimental, but
nowadays is almost unthinkable to use Sledgehammer without it. There are
nevertheless still a few rare cases where one wants to see exactly which
lemmas were used by the prover, and the metis output is then more
informative.
Sledgehammer has a detailed documentation listing all the options, but is
there a description of the everyday use of it?
Email Gateway (Mar 29 2023 at 10:38):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Dear Gergely,
The Sledgehammer documentation includes sections called "Hints" and "Frequently Asked Questions" that attempt to describe the everyday use of the tool. Surely they're not perfect, so I'd be happy to improve them if you have suggestions.
Best,
Jasmin
Last updated: Apr 29 2024 at 01:08 UTC