doc-src/TutorialI/CTL/CTLind.thy

--- a/doc-src/TutorialI/CTL/CTLind.thy	Wed Jan 10 11:07:11 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTLind.thy	Wed Jan 10 11:08:29 2001 +0100
@@ -128,7 +128,7 @@
 @{thm[display]Avoid_in_lfp[no_vars]}
 The main theorem is simply the corollary where @{prop"t = s"},
 in which case the assumption @{prop"t \<in> Avoid s A"} is trivially true
-by the first @{term Avoid}-rule). Isabelle confirms this:
+by the first @{term Avoid}-rule. Isabelle confirms this:
 *}
 
 theorem AF_lemma2: