Ciarán Dunne (Jun 03 2025 at 15:41): Ciarán Dunne (Jun 03 2025 at 15:41):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 30 2025 at 01:55 UTC