[isabelle] Localized Named Theorems
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Localized Named Theorems
- From: Christian Sternagel <c.sternagel at gmail.com>
- Date: Wed, 28 Aug 2013 14:02:01 +0900
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130805 Thunderbird/17.0.8
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 = ...
lemma A [my_thms] ...
interpretation my_l!: l ...
I shortly considered bundles, but as far as I see, those cannot be
extended incrementally. Are there any other ways of achieving something
This archive was generated by a fusion of
Pipermail (Mailman edition) and