Max W. Haslbeck (Sep 25 2019 at 13:23): Max W. Haslbeck (Sep 25 2019 at 13:23):Is there any way to show all theorems with a certain attribute? For example all theorems with the fundef_cong attribute?
Kevin Kappelmann (Sep 26 2019 at 08:12):My "solution" would be grep; but there might be something built-in I'm not aware of
Simon Wimmer (Sep 26 2019 at 12:26):I believe the answer is 'no'.
For standard collections of named theorems, you can do
thm algebra_simps
thm transfer_raw
but for attributes that handle things on their own like fundef_cong,
there shouldn't be a way since attributes are just arbitrary code in the end.
Last updated: Dec 21 2024 at 12:33 UTC