[isabelle-dev] NEWS: restricted name space accesses

[Makarius]

* 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:

   context
   begin

   private definition ...
   private lemma ...

   qualified definition ...
   qualified lemma ...

   lemma ...
   theorem ...

   end


This refers to Isabelle/a81dc82ecba3, and supersedes the NEWS announcement 
about "limited name space accesses", see 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2015-April/005974.html

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 
release.)


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.


 	Makarius