doc-src/Ref/syntax.tex
 changeset 499 5a54c796b808 parent 332 01b87a921967 child 864 d63b111b917a
equal inserted replaced
498:689e2bd78c19 499:5a54c796b808
   421
   421
   422 \item Every variable in~$r$ must also occur in~$l$.
   422 \item Every variable in~$r$ must also occur in~$l$.
   423 \end{itemize}
   423 \end{itemize}
   424
   424
   425 Macro rules may refer to any syntax from the parent theories.  They may
   425 Macro rules may refer to any syntax from the parent theories.  They may
   426 also refer to anything defined before the the {\tt .thy} file's {\tt
   426 also refer to anything defined before the {\tt .thy} file's {\tt
   427   translations} section --- including any mixfix declarations.
   427   translations} section --- including any mixfix declarations.
   428
   428
   429 Upon declaration, both sides of the macro rule undergo parsing and parse
   429 Upon declaration, both sides of the macro rule undergo parsing and parse
   430 \AST{} translations (see \S\ref{sec:asts}), but do not themselves undergo
   430 \AST{} translations (see \S\ref{sec:asts}), but do not themselves undergo
   431 macro expansion.  The lexer runs in a different mode that additionally
   431 macro expansion.  The lexer runs in a different mode that additionally