--- a/doc-src/TutorialI/CTL/Base.thy Wed Oct 11 13:33:38 2000 +0200
+++ b/doc-src/TutorialI/CTL/Base.thy Wed Oct 11 13:39:52 2000 +0200
@@ -5,7 +5,7 @@
text{*
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