is there a way to name the lemmas in a theory? I mean, all the lemmas in one expression to feed it to Sledgehammer.
There is the lemmas command.
lemmas
e.g. lemmas myname = a b c
lemmas myname = a b c
Last updated: Dec 21 2024 at 12:33 UTC