diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/CTL/PDL.thy
--- a/doc-src/TutorialI/CTL/PDL.thy	Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/CTL/PDL.thy	Mon Oct 09 19:20:55 2000 +0200
@@ -1,8 +1,8 @@
 (*<*)theory PDL = Base:(*>*)
 
-subsection{*Propositional dynmic logic---PDL*}
+subsection{*Propositional dynamic logic---PDL*}
 
-text{*
+text{*\index{PDL|(}
 The formulae of PDL are built up from atomic propositions via the customary
 propositional connectives of negation and conjunction and the two temporal
 connectives @{text AX} and @{text EF}. Since formulae are essentially
@@ -60,7 +60,6 @@
 "mc(AX f)    = {s. \<forall>t. (s,t) \<in> M  \<longrightarrow> t \<in> mc f}"
 "mc(EF f)    = lfp(\<lambda>T. mc f \<union> M^-1 ^^ T)"
 
-
 text{*\noindent
 Only the equation for @{term EF} deserves some comments. Remember that the
 postfix @{text"^-1"} and the infix @{text"^^"} are predefined and denote the
@@ -199,6 +198,7 @@
 Show that the semantics for @{term EF} satisfies the following recursion equation:
 @{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"}
 \end{exercise}
+\index{PDL|)}
 *}
 (*<*)
 theorem main: "mc f = {s. s \<Turnstile> f}";