[isabelle-dev] NEWS: auxiliary contexts

Makarius makarius at sketis.net
Tue Apr 17 11:53:11 CEST 2012

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.


More information about the isabelle-dev mailing list