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