1.1 --- a/doc-src/TutorialI/CTL/CTLind.thy	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/CTLind.thy	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -125,7 +125,7 @@
     1.4  
     1.5  text{*
     1.6  The @{text"(no_asm)"} modifier of the @{text"rule_format"} directive means
     1.7 -that the assumption is left unchanged---otherwise the @{text"\<forall>p"} is turned
     1.8 +that the assumption is left unchanged --- otherwise the @{text"\<forall>p"} is turned
     1.9  into a @{text"\<And>p"}, which would complicate matters below. As it is,
    1.10  @{thm[source]Avoid_in_lfp} is now
    1.11  @{thm[display]Avoid_in_lfp[no_vars]}