diff -r e77662e9cabd -r 4c2584e23ade doc-src/TutorialI/CTL/document/Base.tex
--- a/doc-src/TutorialI/CTL/document/Base.tex	Wed Oct 11 13:33:38 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Wed Oct 11 13:39:52 2000 +0200
@@ -7,7 +7,7 @@
 \begin{isamarkuptext}%
 Model checking is a very popular technique for the verification of finite
 state systems (implementations) w.r.t.\ temporal logic formulae
-(specifications) \cite{Clarke,Huth-Ryan-book}. Its foundations are completely set theoretic
+(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic
 and this section shall explore them a little in HOL. This is done in two steps: first
 we consider a simple modal logic called propositional dynamic
 logic (PDL) which we then extend to the temporal logic CTL used in many real