[isabelle-dev] Auxiliary contexts again
makarius at sketis.net
Mon Oct 15 14:20:53 CEST 2012
On Mon, 15 Oct 2012, Christian Sternagel wrote:
> Just out of curiosity. Why is it not allowed to "open" a named context
> inside an auxiliary context?
The question is merely what is feasible to implement. The challenge
increases approximately along the following line of further development:
(0) Non-nested targets and properly localized packages -- more or less
established in the past few years, although some packages are still
lacking localization, and we are still chewing some fine-points concerning
(1) Nested auxiliary contexts inside some outermost target: This is
where we are getting half-way now. The idea is rather old, but early this
year I dared to open this can again.
(2) Properly nested sub-target structure for bundles -- a reletively new
thing, but not fully implemented yet.
(3) Nesting of named targets inside any of the other context blocks
above -- still far ahead and presently out of reach.
More information about the isabelle-dev