# HG changeset patch
# User wenzelm
# Date 1428177690 -7200
# Node ID 003dbac78546bc7032777edbfc76579523d3506d
# Parent  32402fe5ae6a3b7456b1be94dda0ad19771556c4
some explanation of 'private';

diff -r 32402fe5ae6a -r 003dbac78546 NEWS
--- a/NEWS	Sat Apr 04 21:30:58 2015 +0200
+++ b/NEWS	Sat Apr 04 22:01:30 2015 +0200
@@ -6,6 +6,23 @@
 
 *** General ***
 
+* Local theory specifications may have a 'private' modifier to restrict
+name space accesses to the current local scope, as delimited by "context
+begin ... end". For example, this works like this:
+
+  context
+  begin
+
+  private definition ...
+  private definition ...
+  private lemma ...
+
+  lemma ...
+  lemma ...
+  theorem ...
+
+  end
+
 * Command 'experiment' opens an anonymous locale context with private
 naming policy.
 
diff -r 32402fe5ae6a -r 003dbac78546 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Sat Apr 04 21:30:58 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Sat Apr 04 22:01:30 2015 +0200
@@ -114,6 +114,7 @@
   \begin{matharray}{rcll}
     @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
     @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
+    @{keyword_def "private"} \\
   \end{matharray}
 
   A local theory target is a specification context that is managed
@@ -160,6 +161,13 @@
   (global) "end"} has a different meaning: it concludes the theory
   itself (\secref{sec:begin-thy}).
   
+  \item @{keyword "private"} may be given as a modifier to any local theory
+  command (before the command keyword). This limits name space accesses to
+  the current local scope, as determined by the enclosing @{command
+  "context"}~@{keyword "begin"}~\dots~@{command "end"} block. Neither a
+  global theory nor a locale target have such a local scope by themselves:
+  an extra unnamed context is required to use @{keyword "private"} here.
+
   \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any local
   theory command specifies an immediate target, e.g.\ ``@{command
   "definition"}~@{text "(\<IN> c)"}'' or ``@{command "theorem"}~@{text