Gergely Buday (Aug 22 2024 at 08:58): Gergely Buday (Aug 22 2024 at 08:58):Is there a syntax to feed the found theorems of a find_theorems call to Sledgehammer?
lemma "foo" using >> find_theorems " search expression" << sledgehammer
?
Gergely Buday (Aug 22 2024 at 09:37):Probably a way to suppress theorems output and display only theorem names, with only spaces between them?
Last updated: Dec 21 2024 at 12:33 UTC