--- a/doc-src/IsarRef/syntax.tex Thu Feb 28 17:46:46 2002 +0100
+++ b/doc-src/IsarRef/syntax.tex Thu Feb 28 18:09:04 2002 +0100
@@ -256,12 +256,14 @@
$\isarkeyword{syntax}$ (see \S\ref{sec:syn-trans}) support the full range of
general mixfixes and binders.
-\indexouternonterm{infix}\indexouternonterm{mixfix}
+\indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
\begin{rail}
infix: '(' ('infix' | 'infixl' | 'infixr') string? nat ')'
;
mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
;
+ structmixfix: mixfix | '(' 'structure' ')'
+ ;
prios: '[' (nat + ',') ']'
;