1.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Wed Aug 25 11:30:45 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Wed Aug 25 14:18:09 2010 +0200
     1.3 @@ -1262,8 +1262,6 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  \begin{matharray}{rcl}
     1.7 -    \indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     1.8 -    \indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     1.9      \indexdef{}{command}{hide\_class}\hypertarget{command.hide-class}{\hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
    1.10      \indexdef{}{command}{hide\_type}\hypertarget{command.hide-type}{\hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
    1.11      \indexdef{}{command}{hide\_const}\hypertarget{command.hide-const}{\hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
    1.12 @@ -1283,14 +1281,6 @@
    1.13  
    1.14    \begin{description}
    1.15  
    1.16 -  \item \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} change the current
    1.17 -  name declaration mode.  Initially, theories start in \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically qualified by
    1.18 -  the theory name.  Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} causes all
    1.19 -  names to be declared without the theory prefix, until \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} is declared again.
    1.20 -  
    1.21 -  Note that global names are prone to get hidden accidently later,
    1.22 -  when qualified names of the same base name are introduced.
    1.23 -  
    1.24    \item \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}~\isa{names} fully removes class
    1.25    declarations from a given name space; with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}
    1.26    option, only the base name is hidden.  Global (unqualified) names