equal
deleted
inserted
replaced
242 |
242 |
243 |
243 |
244 section {* Mixfix annotations *} |
244 section {* Mixfix annotations *} |
245 |
245 |
246 text {* Mixfix annotations specify concrete \emph{inner syntax} of |
246 text {* Mixfix annotations specify concrete \emph{inner syntax} of |
247 Isabelle types and terms. Some commands such as @{command |
247 Isabelle types and terms. Locally fixed parameters in toplevel |
248 "typedecl"} admit infixes only, while @{command "definition"} etc.\ |
248 theorem statements, locale specifications etc.\ also admit mixfix |
249 support the full range of general mixfixes and binders. Fixed |
249 annotations. |
250 parameters in toplevel theorem statements, locale specifications |
|
251 also admit mixfix annotations. |
|
252 |
250 |
253 \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} |
251 \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} |
254 \begin{rail} |
252 \begin{rail} |
255 infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')' |
253 infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')' |
256 ; |
254 ; |