Gergely Buday (Jun 13 2024 at 14:54): Gergely Buday (Jun 13 2024 at 14:54):I could not find this in the official Sledgehammer documentation:
is there a way to name a theory and Sledgehammer would use all the lemmas from there?
Also: what is Sledgehammer's strategy when it picks theorems?
Mathias Fleury (Jun 15 2024 at 18:34):https://isabelle.in.tum.de/doc/sledgehammer.pdf in the FAQ
Mathias Fleury (Jun 15 2024 at 18:35):and no there is no such way (I do not believe it would make much sense actually)
Last updated: Dec 21 2024 at 16:20 UTC