doc-src/IsarRef/Thy/document/Spec.tex
changeset 36178 0e5c133b48b6
parent 36177 8e0770d2e499
child 36454 f2b5bcc61a8c
     1.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Fri Apr 16 22:15:09 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Fri Apr 16 22:18:59 2010 +0200
     1.3 @@ -990,7 +990,7 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  \begin{matharray}{rcll}
     1.7 -    \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     1.8 +    \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
     1.9      \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
    1.10      \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
    1.11    \end{matharray}