1.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Mon Mar 01 17:09:42 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Mon Mar 01 17:12:43 2010 +0100
     1.3 @@ -378,34 +378,47 @@
     1.4  \end{isamarkuptext}%
     1.5  \isamarkuptrue%
     1.6  %
     1.7 -\isamarkupsection{Explicit term notation%
     1.8 +\isamarkupsection{Explicit notation%
     1.9  }
    1.10  \isamarkuptrue%
    1.11  %
    1.12  \begin{isamarkuptext}%
    1.13  \begin{matharray}{rcll}
    1.14 +    \indexdef{}{command}{type\_notation}\hypertarget{command.type-notation}{\hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
    1.15 +    \indexdef{}{command}{no\_type\_notation}\hypertarget{command.no-type-notation}{\hyperlink{command.no-type-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}type{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
    1.16      \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
    1.17      \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
    1.18    \end{matharray}
    1.19  
    1.20    \begin{rail}
    1.21 +    ('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and')
    1.22 +    ;
    1.23      ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
    1.24      ;
    1.25    \end{rail}
    1.26  
    1.27    \begin{description}
    1.28  
    1.29 +  \item \hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix
    1.30 +  syntax with an existing type constructor.  The arity of the
    1.31 +  constructor is retrieved from the context.
    1.32 +  
    1.33 +  \item \hyperlink{command.no-type-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}type{\isacharunderscore}notation}}}} is similar to \hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}, but removes the specified syntax annotation from
    1.34 +  the present context.
    1.35 +
    1.36    \item \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix
    1.37 -  syntax with an existing constant or fixed variable.  This is a
    1.38 -  robust interface to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} primitive
    1.39 -  (\secref{sec:syn-trans}).  Type declaration and internal syntactic
    1.40 -  representation of the given entity is retrieved from the context.
    1.41 +  syntax with an existing constant or fixed variable.  The type
    1.42 +  declaration of the given entity is retrieved from the context.
    1.43    
    1.44    \item \hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}},
    1.45    but removes the specified syntax annotation from the present
    1.46    context.
    1.47  
    1.48 -  \end{description}%
    1.49 +  \end{description}
    1.50 +
    1.51 +  Compared to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} and \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}} primitives (\secref{sec:syn-trans}), the above commands
    1.52 +  provide explicit checking wrt.\ the logical context, and work within
    1.53 +  general local theory targets, not just the global theory.%
    1.54  \end{isamarkuptext}%
    1.55  \isamarkuptrue%
    1.56  %