[isabelle-dev] NEWS: auxiliary contexts
makarius at sketis.net
Mon Apr 16 12:26:17 CEST 2012
On Mon, 16 Apr 2012, Brian Huffman wrote:
> Finally we have a mechanism similar to "Section" in Coq, a more
> lightweight alternative to locales.
This is what Larry Paulson and Florian Kammüller actually started in
1998/1999 and eventually became the fully-featured locale + interpretation
system of today. The basic contexts are useful independently of that,
especially since they can be nested within themselves and the other
The nesting is also where some small problems might still persist, since
the Haftmann-Wenzel sandwich looks now like a Neapolitan wafer.
> I already replaced a one-off locale with this new local context
> (changeset 4d49f3ffe97e)
In that change you also group several "(in c)" into a single "context v
begin ... end". This generally helps to improve scalability of locale
applications, since context switching is realatively heavy.
At some point I would like to see Isabelle/jEdit in assisting to manage
such context rearrangements.
More information about the isabelle-dev