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