Re: [isabelle] Locales and bundles in Isabelle – a short comparion
There's another difference between locales and bundles: locales can be extended at any
time whereas one cannot change a bundle after its declaration.
On 28/01/14 10:14, Florian Haftmann wrote:
with the presence of »confined interpretation« in Isabelle, I asked
myself how this relates to the already existing declaration bundles.
See also attached theory.
* Conceptually, confined interpretation absorbs declaration bundles
* Not covered are declaration bundles defined *inside* a locale since
locales are not nestable.
* There is a subtle structural difference:
a) confined interpretation can happen incrementally at arbitrary
positions inside the nested context;
b) inclusion of bundles can only happen at the beginning of a nested
However, this does not make really a difference since you are always
free to open a new nested context if needed. I.e.
This might suggest a declaration »inclusion« which includes a
declaration bundle up to the end of the current nested context, similar
to interpretation, e.g.
This archive was generated by a fusion of
Pipermail (Mailman edition) and