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