changeset 499 | 5a54c796b808 |
parent 332 | 01b87a921967 |
child 864 | d63b111b917a |
--- a/doc-src/Ref/syntax.tex Fri Jul 29 13:28:39 1994 +0200 +++ b/doc-src/Ref/syntax.tex Fri Jul 29 13:30:48 1994 +0200 @@ -423,7 +423,7 @@ \end{itemize} Macro rules may refer to any syntax from the parent theories. They may -also refer to anything defined before the the {\tt .thy} file's {\tt +also refer to anything defined before the {\tt .thy} file's {\tt translations} section --- including any mixfix declarations. Upon declaration, both sides of the macro rule undergo parsing and parse