[isabelle-dev] NEWS: bundled declarations
makarius at sketis.net
Thu Apr 26 22:40:42 CEST 2012
On Tue, 24 Apr 2012, Brian Huffman wrote:
> On Sun, Apr 15, 2012 at 3:00 PM, Makarius <makarius at sketis.net> wrote:
>> * Bundled declarations associate attributed fact expressions with a
>> given name in the context. These may be later included in other
>> contexts. This allows to manage context extensions casually, without
>> the logical dependencies of locales and locale interpretation.
> This seems like a really nice feature! I think it will be especially
> useful in combination with local context blocks.
The bundles have much more potential than implemented so far, say for
substructuring theories or locales, both from the organizational viewpoint
and scalability (since declarations can "bundled" and not applied only on
We need to come back to this later, after the official rollout of
More information about the isabelle-dev