diff -r 5bea3a8abdc3 -r 08188224c24e doc-src/TutorialI/CTL/document/PDL.tex
--- a/doc-src/TutorialI/CTL/document/PDL.tex	Wed Mar 14 18:40:01 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/PDL.tex	Thu Mar 15 10:41:32 2001 +0100
@@ -7,8 +7,10 @@
 %
 \begin{isamarkuptext}%
 \index{PDL|(}
-The formulae of PDL are built up from atomic propositions via the customary
-propositional connectives of negation and conjunction and the two temporal
+The formulae of PDL\footnote{The customary definition of PDL
+\cite{HarelKT-DL} looks quite different from ours, but the two are easily
+shown to be equivalent.} are built up from atomic propositions via
+negation and conjunction and the two temporal
 connectives \isa{AX} and \isa{EF}. Since formulae are essentially
 syntax trees, they are naturally modelled as a datatype:%
 \end{isamarkuptext}%