[isabelle-dev] NEWS

[Clemens Ballarin]

The upcoming release (which I guess will be called Isabelle 2011-0  
Dispensable Debate) will have the following notable extensions to  
locale interpretation:

* Locale interpretation commands 'interpret' and 'sublocale' accept
lists of equations to map definitions in a locale to appropriate
entities in the context of the interpretation.  The 'interpretation'
command already provided this functionality.

* New diagnostic command 'print_dependencies' prints the locale
instances that would be activated if the specified expression was
interpreted in the current context.  Variant 'print_dependencies!'
assumes a context without interpretations.

The mixins for the sublocale command feature (first item above) is a  
bit experimental.  In particular, it does not provide inheritance of  
mixins as interpretation and interpret do.  It is not yet clear to me  
how to best do this.  In any case, future extensions are expected to  
be compatible to the current state.

Clemens