Email Gateway (Aug 19 2022 at 11:44): 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: Apr 25 2024 at 08:20 UTC