doc-src/Ref/syntax.tex

 
 \item Every variable in~$r$ must also occur in~$l$.
 \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
 \AST{} translations (see \S\ref{sec:asts}), but do not themselves undergo
 macro expansion.  The lexer runs in a different mode that additionally