doc-src/IsarRef/pure.tex
changeset 26660 f978a6f48949
parent 26479 3a2efce3e992
--- a/doc-src/IsarRef/pure.tex	Tue Apr 15 16:25:14 2008 +0200
+++ b/doc-src/IsarRef/pure.tex	Tue Apr 15 18:49:12 2008 +0200
@@ -452,10 +452,10 @@
   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$] fully removes declarations from a
-  given name space (which may be $class$, $type$, or $const$); with the
-  $(open)$ option, only the base name is hidden.  Global (unqualified) names
-  may never be hidden.
+\item [$\isarkeyword{hide}~space~names$] fully removes declarations
+  from a given name space (which may be $class$, $type$, $const$, or
+  $fact$); with the $(open)$ option, only the base name is hidden.
+  Global (unqualified) names may never be hidden.
   
   Note that hiding name space accesses has no impact on logical declarations
   -- they remain valid internally.  Entities that are no longer accessible to