# HG changeset patch
# User wenzelm
# Date 1208278152 -7200
# Node ID f978a6f489496322a4ea2ff73dd84953d957d575
# Parent  aae01f2139af05f0347d9781ae198d11fd40f366
added hide fact;

diff -r aae01f2139af -r f978a6f48949 NEWS
--- a/NEWS	Tue Apr 15 16:25:14 2008 +0200
+++ b/NEWS	Tue Apr 15 18:49:12 2008 +0200
@@ -40,6 +40,8 @@
 that tools may maintain dynamically scoped facts systematically, using
 PureThy.add_thms_dynamic.
 
+* Command 'hide' now allows to hide from "fact" name space as well.
+
 * Eliminated destructive theorem database, simpset, claset, and
 clasimpset.  Potential INCOMPATIBILITY, really need to observe linear
 update of theories within ML code.
diff -r aae01f2139af -r f978a6f48949 doc-src/IsarRef/pure.tex
--- 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