diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/CTL/Base.thy
--- a/doc-src/TutorialI/CTL/Base.thy	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/CTL/Base.thy	Tue Oct 31 08:53:12 2000 +0100
@@ -2,7 +2,7 @@
 
 section{*Case study: Verified model checking*}
 
-text{*
+text{*\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