doc-src/TutorialI/CTL/CTL.thy
changeset 10192 4c2584e23ade
parent 10186 499637e8f2c6
child 10210 e8aa81362f41
--- a/doc-src/TutorialI/CTL/CTL.thy	Wed Oct 11 13:33:38 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy	Wed Oct 11 13:39:52 2000 +0200
@@ -386,7 +386,7 @@
 %{text[display]"| EU formula formula    E[_ U _]"}
 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
 \end{exercise}
-For more CTL exercises see, for example \cite{Huth-Ryan-book,Clarke-as-well?}.
+For more CTL exercises see, for example \cite{Huth-Ryan-book}.
 \bigskip
 
 Let us close this section with a few words about the executability of our model checkers.