NEWS
changeset 59990 a81dc82ecba3
parent 59967 2fcf41a626f7
child 59991 09be0495dcc2
     1.1 --- a/NEWS	Thu Apr 09 15:54:09 2015 +0200
     1.2 +++ b/NEWS	Thu Apr 09 20:42:32 2015 +0200
     1.3 @@ -7,17 +7,18 @@
     1.4  *** General ***
     1.5  
     1.6  * Local theory specification commands may have a 'private' or
     1.7 -'restricted' modifier to limit name space accesses to the local scope,
     1.8 +'qualified' modifier to restrict name space accesses to the local scope,
     1.9  as provided by some "context begin ... end" block. For example:
    1.10  
    1.11    context
    1.12    begin
    1.13  
    1.14    private definition ...
    1.15 -  private definition ...
    1.16    private lemma ...
    1.17  
    1.18 -  lemma ...
    1.19 +  qualified definition ...
    1.20 +  qualified lemma ...
    1.21 +
    1.22    lemma ...
    1.23    theorem ...
    1.24