1.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 21:52:09 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 21:52:59 2008 +0100
     1.3 @@ -246,11 +246,11 @@
     1.4  section {* Mixfix annotations *}
     1.5  
     1.6  text {* Mixfix annotations specify concrete \emph{inner syntax} of
     1.7 -  Isabelle types and terms.  Some commands such as @{command "types"}
     1.8 -  (see \secref{sec:types-pure}) admit infixes only, while @{command
     1.9 -  "consts"} (see \secref{sec:consts}) and @{command "syntax"} (see
    1.10 -  \secref{sec:syn-trans}) support the full range of general mixfixes
    1.11 -  and binders.
    1.12 +  Isabelle types and terms.  Some commands such as @{command
    1.13 +  "typedecl"} admit infixes only, while @{command "definition"} etc.\
    1.14 +  support the full range of general mixfixes and binders.  Fixed
    1.15 +  parameters in toplevel theorem statements, locale specifications
    1.16 +  also admit mixfix annotations.
    1.17  
    1.18    \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
    1.19    \begin{rail}