src/Doc/Isar_Ref/Spec.thy
changeset 59939 7d46aa03696e
parent 59926 003dbac78546
child 59990 a81dc82ecba3
     1.1 --- a/src/Doc/Isar_Ref/Spec.thy	Mon Apr 06 17:28:07 2015 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Mon Apr 06 22:11:01 2015 +0200
     1.3 @@ -115,6 +115,7 @@
     1.4      @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
     1.5      @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
     1.6      @{keyword_def "private"} \\
     1.7 +    @{keyword_def "restricted"} \\
     1.8    \end{matharray}
     1.9  
    1.10    A local theory target is a specification context that is managed
    1.11 @@ -161,12 +162,16 @@
    1.12    (global) "end"} has a different meaning: it concludes the theory
    1.13    itself (\secref{sec:begin-thy}).
    1.14    
    1.15 -  \item @{keyword "private"} may be given as a modifier to any local theory
    1.16 -  command (before the command keyword). This limits name space accesses to
    1.17 -  the current local scope, as determined by the enclosing @{command
    1.18 -  "context"}~@{keyword "begin"}~\dots~@{command "end"} block. Neither a
    1.19 -  global theory nor a locale target have such a local scope by themselves:
    1.20 -  an extra unnamed context is required to use @{keyword "private"} here.
    1.21 +  \item @{keyword "private"} or @{keyword "restricted"} may be given as
    1.22 +  modifiers before any local theory command. This limits name space accesses
    1.23 +  to the local scope, as determined by the enclosing @{command
    1.24 +  "context"}~@{keyword "begin"}~\dots~@{command "end"} block. Outside its
    1.25 +  scope, a @{keyword "private"} name is inaccessible, and a @{keyword
    1.26 +  "restricted"} name is only accessible with additional qualification.
    1.27 +
    1.28 +  Neither a global @{command theory} nor a @{command locale} target provides
    1.29 +  a local scope by itself: an extra unnamed context is required to use
    1.30 +  @{keyword "private"} or @{keyword "restricted"} here.
    1.31  
    1.32    \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any local
    1.33    theory command specifies an immediate target, e.g.\ ``@{command