Stream: General

Topic: Pretty printing definitions/theorems/abbreviation


view this post on Zulip 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 08 2025 at 08:25 UTC