[isabelle-dev] NEWS: bundle target and unbundle command

[Makarius]

*** General ***

* Command 'bundle' provides a local theory target to define a bundle
from the body of specification commands (such as 'declare',
'declaration', 'notation', 'lemmas', 'lemma'). For example:

bundle foo
begin
  declare a [simp]
  declare b [intro]
end

* Command 'unbundle' is like 'include', but works within a local theory
context. Unlike "context includes ... begin", the effect of 'unbundle'
on the target context persists, until different declarations are given.


*** HOL ***

* Library/FinFun.thy: bundles "finfun_syntax" and "no_finfun_syntax"
allow to control optional syntax in local contexts; this supersedes
former Library/FinFun_Syntax.thy. INCOMPATIBILITY, e.g. use "unbundle
finfun_syntax" to imitate import of "~~/src/HOL/Library/FinFun_Syntax".


This refers to Isabelle/a59801b7f125, which also contains the
funfun_syntax bundles that may serve here as canonical examples.


	Makarius