Stream: Isabelle/ML

Topic: all theorems introduced in a theory


view this post on Zulip 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.

view this post on Zulip 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: Jul 15 2022 at 23:21 UTC