do not mention unqualified names, now that 'global' and 'local' are gone
authorkrauss
Sun Oct 10 23:16:24 2010 +0200 (2010-10-10)
changeset 39977c9cbc16e93ce
parent 39976 2474347538b8
child 39978 11bfb7e7cc86
do not mention unqualified names, now that 'global' and 'local' are gone
doc-src/IsarRef/Thy/Spec.thy
doc-src/IsarRef/Thy/document/Spec.tex
     1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Sun Oct 10 16:34:20 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Sun Oct 10 23:16:24 2010 +0200
     1.3 @@ -1209,8 +1209,7 @@
     1.4  
     1.5    \item @{command "hide_class"}~@{text names} fully removes class
     1.6    declarations from a given name space; with the @{text "(open)"}
     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
     2.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Sun Oct 10 16:34:20 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sun Oct 10 23:16:24 2010 +0200
     2.3 @@ -1252,8 +1252,7 @@
     2.4  
     2.5    \item \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}~\isa{names} fully removes class
     2.6    declarations from a given name space; with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}
     2.7 -  option, only the base name is hidden.  Global (unqualified) names
     2.8 -  may never be hidden.
     2.9 +  option, only the base name is hidden.
    2.10  
    2.11    Note that hiding name space accesses has no impact on logical
    2.12    declarations --- they remain valid internally.  Entities that are no