* 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
