[isabelle-dev] Auxiliary contexts again

[Christian Sternagel]

Dear Makarius,

On 10/13/2012 05:34 AM, Makarius wrote:
> Here are some leftovers from the last release concerning the nested
> auxiliary contexts:
>
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/msg00032.html
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/msg00052.html
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/msg00032.html
What was the 3rd message you wanted to refer to?
>
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/msg00045.html
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/msg00047.html
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/msg00035.html
>
> The first three are should somehow work in Isabelle/18cb42182d3e, the
> others are still unclear.  Are there further issues still pending?
Just out of curiosity. Why is it not allowed to "open" a named context 
inside an auxiliary context?

(Again, my use-case is document preparation: I want to describe a locale 
that I have defined in a different theory and therefore have to "open" 
it... however, the locale is only relevant in one subsection, whereas I 
have an auxiliary context "around" the whole document which fixes some 
notation.)
>
>
> This is all from our National Debts department in some sense, and should
> at least become a bit better with every release.
>
>
>      Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev