Qiyuan Xu (Dec 02 2021 at 09:03): Qiyuan Xu (Dec 02 2021 at 09:03):How to get all theorems introduced in a theory, excluding those inherited from father theories?
I know 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.
Qiyuan Xu (Dec 02 2021 at 09:08):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 21 2024 at 16:20 UTC