equal
deleted
inserted
replaced
264 } |
264 } |
265 \isamarkuptrue% |
265 \isamarkuptrue% |
266 % |
266 % |
267 \begin{isamarkuptext}% |
267 \begin{isamarkuptext}% |
268 Mixfix annotations specify concrete \emph{inner syntax} of |
268 Mixfix annotations specify concrete \emph{inner syntax} of |
269 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.\ |
269 Isabelle types and terms. Locally fixed parameters in toplevel |
270 support the full range of general mixfixes and binders. Fixed |
270 theorem statements, locale specifications etc.\ also admit mixfix |
271 parameters in toplevel theorem statements, locale specifications |
271 annotations. |
272 also admit mixfix annotations. |
|
273 |
272 |
274 \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} |
273 \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} |
275 \begin{rail} |
274 \begin{rail} |
276 infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')' |
275 infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')' |
277 ; |
276 ; |