# HG changeset patch
# User lcp
# Date 775481448 -7200
# Node ID 5a54c796b80881a91f06dcd2951ad0b820aa3389
# Parent  689e2bd78c1972a04904f8bec2c06d5fe6664df2
deleted repeated "the" in "before the the .thy file"

diff -r 689e2bd78c19 -r 5a54c796b808 doc-src/Ref/syntax.tex
--- 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