By issuing the
sledgehammer command one calls automatic theorem provers (ATPs) and satisfiability-modulo-theories (SMT) solvers on the current goal. Instead of issuing the sledgehammer command one can use the Sledgehammer menu at the bottom of jEdit to open the Sledgehammer panel and then press Apply.
The problem passed to the solvers consists of your current goal together with an automatic selection of facts from the theory context.
However, with the
using command one can pass his own selection of relevant definitions and lemmas in order to help Sledgehammer to solve the current goal.
To learn more about Sledgehammer one can read the user's guide to Sledgehammer.
Last updated: Dec 07 2023 at 08:19 UTC