What good ways are there to uniformaly print a list of definitions/theorems/abbreviations preceded by their names in Isabelle/HOL?
For example, I might have a bunch of defined constants, and I want to see all of their definitions together in the output panel. For this, I can use the lemmas
command and just put lemmas foo_def bar_def
, but if foo
has syntax it would be nice to see the text foo_def
next to the equation like with find_theorems
.
I suppose I could just write a custom ML command for this, but it seems like something that Isabelle already does.
Thanks!
Last updated: Jun 08 2025 at 08:25 UTC