ballarin at in.tum.de
Fri Jan 7 12:43:44 CET 2011
The upcoming release (which I guess will be called Isabelle 2011-0
Dispensable Debate) will have the following notable extensions to
* 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.
More information about the isabelle-dev