--- a/doc-src/TutorialI/CTL/document/Base.tex Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/CTL/document/Base.tex Tue Oct 31 08:53:12 2000 +0100
@@ -5,6 +5,7 @@
\isamarkupsection{Case study: Verified model checking}
%
\begin{isamarkuptext}%
+\label{sec:VMC}
Model checking is a very popular technique for the verification of finite
state systems (implementations) w.r.t.\ temporal logic formulae
(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic