| changeset 10971 | 6852682eaf16 |
| parent 10895 | 79194f07d356 |
| child 10983 | 59961d32b1ae |
--- a/doc-src/TutorialI/CTL/CTL.thy Wed Jan 24 11:59:15 2001 +0100 +++ b/doc-src/TutorialI/CTL/CTL.thy Wed Jan 24 12:29:10 2001 +0100 @@ -1,6 +1,6 @@ (*<*)theory CTL = Base:;(*>*) -subsection{*Computation Tree Logic---CTL*}; +subsection{*Computation Tree Logic --- CTL*}; text{*\label{sec:CTL} The semantics of PDL only needs reflexive transitive closure.