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

Makarius makarius at sketis.net
Fri Jun 10 23:58:14 CEST 2016

*** 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
  declare a [simp]
  declare b [intro]

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


More information about the isabelle-dev mailing list