src/Doc/Tutorial/CTL/PDL.thy

--- a/src/Doc/Tutorial/CTL/PDL.thy	Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/CTL/PDL.thy	Tue Oct 07 22:35:11 2014 +0200
@@ -8,7 +8,7 @@
 connectives @{text AX} and @{text EF}\@. Since formulae are essentially
 syntax trees, they are naturally modelled as a datatype:%
 \footnote{The customary definition of PDL
-\cite{HarelKT-DL} looks quite different from ours, but the two are easily
+@{cite "HarelKT-DL"} looks quite different from ours, but the two are easily
 shown to be equivalent.}
 *}