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.

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: Jun 20 2024 at 12:31 UTC