# HG changeset patch
# User wenzelm
# Date 955973331 -7200
# Node ID 7b15f4bdd72fab027d9bf8dbfebb8d746a5b4cda
# Parent  0e48ee5b52db358d4d80e309f6fbed3a4e33e101
'global' / 'local': comment;
added 'hide';

diff -r 0e48ee5b52db -r 7b15f4bdd72f doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Mon Apr 17 14:08:19 2000 +0200
+++ b/doc-src/IsarRef/pure.tex	Mon Apr 17 14:08:51 2000 +0200
@@ -319,16 +319,26 @@
 
 \subsection{Name spaces}
 
-\indexisarcmd{global}\indexisarcmd{local}
+\indexisarcmd{global}\indexisarcmd{local}\indexisarcmd{hide}
 \begin{matharray}{rcl}
   \isarcmd{global} & : & \isartrans{theory}{theory} \\
   \isarcmd{local} & : & \isartrans{theory}{theory} \\
+  \isarcmd{hide} & : & \isartrans{theory}{theory} \\
 \end{matharray}
 
+\begin{rail}
+  'global' comment?
+  ;
+  'local' comment?
+  ;
+  'hide' name (nameref + ) comment?
+  ;
+\end{rail}
+
 Isabelle organizes any kind of name declarations (of types, constants,
 theorems etc.) by separate hierarchically structured name spaces.  Normally
-the user never has to control the behavior of name space entry by hand, yet
-the following commands provide some way to do so.
+the user does not have to control the behavior of name spaces by hand, yet the
+following commands provide some way to do so.
 
 \begin{descr}
 \item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current
@@ -336,6 +346,17 @@
   mode, causing all names to be automatically qualified by the theory name.
   Changing this to $\isarkeyword{global}$ causes all names to be declared
   without the theory prefix, until $\isarkeyword{local}$ is declared again.
+  
+  Note that global names are prone to get hidden accidently later, when
+  qualified names of the same base name are introduced.
+  
+\item [$\isarkeyword{hide}~space~names$] removes declarations from a given
+  name space (which may be $class$, $type$, or $const$).  Hidden objects
+  remain valid within the logic, but are inaccessible from user input.  In
+  output, the special qualifier ``$\mathord?\mathord?$'' is prefixed to the
+  full internal name.
+  
+  Unqualified (global) names may not be hidden deliberately.
 \end{descr}