doc-src/IsarRef/Thy/document/Spec.tex
changeset 35681 8b22a498b034
parent 35351 7425aece4ee3
child 36177 8e0770d2e499
     1.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Tue Mar 09 23:29:04 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Tue Mar 09 23:32:13 2010 +0100
     1.3 @@ -991,7 +991,7 @@
     1.4  \begin{isamarkuptext}%
     1.5  \begin{matharray}{rcll}
     1.6      \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     1.7 -    \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     1.8 +    \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
     1.9      \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
    1.10    \end{matharray}
    1.11