--- a/NEWS Thu Apr 09 18:46:16 2015 +0200
+++ b/NEWS Thu Apr 09 20:42:38 2015 +0200
@@ -7,17 +7,18 @@
*** General ***
* Local theory specification commands may have a 'private' or
-'restricted' modifier to limit name space accesses to the local scope,
+'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 definition ...
private lemma ...
- lemma ...
+ qualified definition ...
+ qualified lemma ...
+
lemma ...
theorem ...