1.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Sun Nov 28 15:34:35 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sun Nov 28 16:15:31 2010 +0100
     1.3 @@ -273,11 +273,12 @@
     1.4  
     1.5    \begin{matharray}{rcl}
     1.6      \indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
     1.7 +    \indexdef{}{command}{syntax\_declaration}\hypertarget{command.syntax-declaration}{\hyperlink{command.syntax-declaration}{\mbox{\isa{\isacommand{syntax{\isaliteral{5F}{\isacharunderscore}}declaration}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
     1.8      \indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
     1.9    \end{matharray}
    1.10  
    1.11    \begin{rail}
    1.12 -    'declaration' ('(pervasive)')? target? text
    1.13 +    ('declaration' | 'syntax_declaration') ('(pervasive)')? target? text
    1.14      ;
    1.15      'declare' target? (thmrefs + 'and')
    1.16      ;
    1.17 @@ -295,6 +296,9 @@
    1.18    declaration is applied to all possible contexts involved, including
    1.19    the global background theory.
    1.20  
    1.21 +  \item \hyperlink{command.syntax-declaration}{\mbox{\isa{\isacommand{syntax{\isaliteral{5F}{\isacharunderscore}}declaration}}}} is similar to \hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}, but is meant to affect only ``syntactic'' tools by
    1.22 +  convention (such as notation and type-checking information).
    1.23 +
    1.24    \item \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms} declares theorems to the
    1.25    current local theory context.  No theorem binding is involved here,
    1.26    unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\