deleted repeated "the" in "before the the .thy file"
authorlcp
Fri, 29 Jul 1994 13:30:48 +0200
changeset 499 5a54c796b808
parent 498 689e2bd78c19
child 500 0842a38074e7
deleted repeated "the" in "before the the .thy file"
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