[isabelle-dev] NEWS: restricted name space accesses
makarius at sketis.net
Thu Apr 9 21:38:23 CEST 2015
* Local theory specification commands may have a 'private' or 'qualified'
modifier to restrict name space accesses to the local scope, as provided
by some "context begin ... end" block. For example:
private definition ...
private lemma ...
qualified definition ...
qualified lemma ...
This refers to Isabelle/a81dc82ecba3, and supersedes the NEWS announcement
about "limited name space accesses", see
The examples above merely use the very simple specification mechanisms of
'definition' and 'theorem', but of course it should work with any other
definitional package, as long as it conforms to usual local_theory
disciplines. (A known exception is 'datatype' due to its use of
Local_Theory.restore in the middle, but this won't change for this
When updating old theories to eliminate "hide" or "hide (open)", one needs
to keep in mind that the above qualification affects all names, e.g. for
'definition' both the defined const and its defining fact.
There is no particularly need to update anything right now. Starting the
release process has priority over fine-tuning of existing theories.
More information about the isabelle-dev