[isabelle-dev] Auxiliary contexts again
c-sterna at jaist.ac.jp
Mon Oct 15 07:22:09 CEST 2012
On 10/13/2012 05:34 AM, Makarius wrote:
> Here are some leftovers from the last release concerning the nested
> auxiliary contexts:
What was the 3rd message you wanted to refer to?
> 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
> This is all from our National Debts department in some sense, and should
> at least become a bit better with every release.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev