[isabelle-dev] NEWS: auxiliary contexts

[Makarius]

On Tue, 17 Apr 2012, Lawrence Paulson wrote:

> I look forward to seeing some documentation on these increasingly 
> mysterious constructs… :-)

It is pretty close to the original concept of "section" that you've 
introduced with Florian Kammüller in 1998/1999, so it is much more basic 
than locales + locale interpretation.

The Isabelle/a83b25e5bad3 changeset of the announcement also covers the 
documentation in the isar-ref manual.  It is quite compact, but that is it 
for now.  For the user it is mainly a new presentation of long established 
concepts anyway.


 	Makarius