doc-src/IsarRef/Thy/document/Spec.tex

     \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
   \end{matharray}
 
   \begin{rail}
-    'types' (typespec '=' type infix? +)
-    ;
-    'typedecl' typespec infix?
+    'types' (typespec '=' type mixfix? +)
+    ;
+    'typedecl' typespec mixfix?
     ;
     'arities' (nameref '::' arity +)
     ;
   \end{rail}