Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Localized Named Theorems

Email Gateway (Aug 19 2022 at 11:44):

From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,

is there a localized variant of the ML-Functor Named_Thms? What I mean
by that is that after setting up a name, e.g., "my_thms", I want to be
able to retrieve specific versions of those theorems. Consider

locale l = ...
begin

lemma A [my_thms] ...

thm my_thms

end

thm l.my_thms

interpretation my_l!: l ...

thm my_l.my_thms

I shortly considered bundles, but as far as I see, those cannot be
extended incrementally. Are there any other ways of achieving something
similar?

cheers

chris

Last updated: Nov 21 2024 at 12:39 UTC