--- a/doc-src/IsarRef/Thy/Spec.thy Sun Oct 10 16:34:20 2010 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Sun Oct 10 23:16:24 2010 +0200
@@ -1209,8 +1209,7 @@
\item @{command "hide_class"}~@{text names} fully removes class
declarations from a given name space; with the @{text "(open)"}
- option, only the base name is hidden. Global (unqualified) names
- may never be hidden.
+ option, only the base name is hidden.
Note that hiding name space accesses has no impact on logical
declarations --- they remain valid internally. Entities that are no
--- a/doc-src/IsarRef/Thy/document/Spec.tex Sun Oct 10 16:34:20 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Sun Oct 10 23:16:24 2010 +0200
@@ -1252,8 +1252,7 @@
\item \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}~\isa{names} fully removes class
declarations from a given name space; with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}
- option, only the base name is hidden. Global (unqualified) names
- may never be hidden.
+ option, only the base name is hidden.
Note that hiding name space accesses has no impact on logical
declarations --- they remain valid internally. Entities that are no