[isabelle-dev] NEWS: restricted name space accesses

Makarius 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 ...

   lemma ...
   theorem ...


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 mailing list