author | lcp |
Fri, 29 Jul 1994 13:30:48 +0200 | |
changeset 499 | 5a54c796b808 |
parent 498 | 689e2bd78c19 |
child 500 | 0842a38074e7 |
--- 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