[isabelle-dev] NEWS: bundled declarations

[Makarius]

* 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.

See commands 'bundle', 'include', 'including' etc. in the isar-ref
manual.


This refers to Isabelle/e94cc23d434a.  It is another old idea that has 
come up occasionally, e.g. as "hintsets" in 2010.

The present implementation is rather modest, only for closed expressions 
of theorems with attributes.  It can conceptually be extended to a full 
target on its own, e.g. to allow bundling of notation, probably also 
logical definitions and theorems.  Moreover, a future version could 
maintain bundles internally as lazy context declarations, to help 
improving scalability of locales by subdividing the body.  This is only 
the starting point for further applications that can be anticipated.

Right now, what is also notable is that the 'includes' element for 
'context' and 'theorem' statements is fully evaluated before any other 
context element.  So earlier workarounds via 'notes' should now work 
better via 'includes', say to modify syntax or type-checking before 
building up the logical context of a long theorem statement.


 	Makarius