--- a/doc-src/TutorialI/CTL/CTLind.thy Thu Oct 19 21:25:15 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTLind.thy Fri Oct 20 08:46:41 2000 +0200
@@ -3,12 +3,15 @@
subsection{*CTL revisited*}
text{*\label{sec:CTL-revisited}
+The purpose of this section is twofold: we want to demonstrate
+some of the induction principles and heuristics discussed above and we want to
+show how inductive definitions can simplify proofs.
In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
model checker for CTL. In particular the proof of the
@{thm[source]infinity_lemma} on the way to @{thm[source]AF_lemma2} is not as
simple as one might intuitively expect, due to the @{text SOME} operator
-involved. The purpose of this section is to show how an inductive definition
-can help to simplify the proof of @{thm[source]AF_lemma2}.
+involved. Below we give a simpler proof of @{thm[source]AF_lemma2}
+based on an auxiliary inductive definition.
Let us call a (finite or infinite) path \emph{@{term A}-avoiding} if it does
not touch any node in the set @{term A}. Then @{thm[source]AF_lemma2} says