1.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Feb 24 07:06:39 2010 -0800
     1.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Feb 24 20:37:01 2010 +0100
     1.3 @@ -266,10 +266,9 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  Mixfix annotations specify concrete \emph{inner syntax} of
     1.7 -  Isabelle types and terms.  Some commands such as \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} admit infixes only, while \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}} etc.\
     1.8 -  support the full range of general mixfixes and binders.  Fixed
     1.9 -  parameters in toplevel theorem statements, locale specifications
    1.10 -  also admit mixfix annotations.
    1.11 +  Isabelle types and terms.  Locally fixed parameters in toplevel
    1.12 +  theorem statements, locale specifications etc.\ also admit mixfix
    1.13 +  annotations.
    1.14  
    1.15    \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
    1.16    \begin{rail}