diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Tutorial/CTL/Base.thy
--- a/src/Doc/Tutorial/CTL/Base.thy	Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/CTL/Base.thy	Tue Oct 07 22:35:11 2014 +0200
@@ -7,7 +7,7 @@
 Computation Tree Logic (CTL), a temporal logic.
 Model checking is a popular technique for the verification of finite
 state systems (implementations) with respect to temporal logic formulae
-(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are set theoretic
+(specifications) @{cite "ClarkeGP-book" and "Huth-Ryan-book"}. Its foundations are set theoretic
 and this section will explore them in HOL\@. This is done in two steps.  First
 we consider a simple modal logic called propositional dynamic
 logic (PDL)\@.  We then proceed to the temporal logic CTL, which is