[isabelle-dev] NEWS: bundled declarations

Makarius 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 mailing list