* 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
