[isabelle-dev] NEWS: bundled declarations

[Makarius]

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 
demand).

We need to come back to this later, after the official rollout of 
Isabelle2012.


 	Makarius