Anthony Bordg (Jul 26 2019 at 21:47): Anthony Bordg (Jul 26 2019 at 21:47):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 21 2024 at 12:33 UTC