# 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