[isabelle] Localized Named Theorems



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.