--- a/doc-src/Logics/intro.tex Thu Nov 11 12:44:43 1993 +0100
+++ b/doc-src/Logics/intro.tex Thu Nov 11 13:18:49 1993 +0100
@@ -13,7 +13,7 @@
axioms~\cite{suppes72}. It is built upon classical~\FOL{}.
{\ttindexbold{HOL}} is the higher-order logic of Church~\cite{church40},
-which is also implemented by Gordon's~{\sc hol} system~\cite{gordon88a}. This
+which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon88a}. This
object-logic should not be confused with Isabelle's meta-logic, which is
also a form of higher-order logic.