How to get all theorems introduced in a theory, excluding those inherited from father theories?
Global_Theory.all_thms_of gives all theorems contained in a theory, also including those from fathers, but I haven't found a clever way to filter those introduced in this theory.
Maybe I also recognize some troubles with dynamic theorems. It seems that I can only get a 'snapshot' of theorems at a moment, because of those dynamic theorems.
Last updated: Dec 07 2023 at 16:21 UTC