--- 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.
--- 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