--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Wed Feb 24 07:06:39 2010 -0800
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Wed Feb 24 20:37:01 2010 +0100
@@ -266,10 +266,9 @@
%
\begin{isamarkuptext}%
Mixfix annotations specify concrete \emph{inner syntax} of
- 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.\
- support the full range of general mixfixes and binders. Fixed
- parameters in toplevel theorem statements, locale specifications
- also admit mixfix annotations.
+ Isabelle types and terms. Locally fixed parameters in toplevel
+ theorem statements, locale specifications etc.\ also admit mixfix
+ annotations.
\indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
\begin{rail}