equal
deleted
inserted
replaced
6 The formulae of PDL are built up from atomic propositions via |
6 The formulae of PDL are built up from atomic propositions via |
7 negation and conjunction and the two temporal |
7 negation and conjunction and the two temporal |
8 connectives @{text AX} and @{text EF}\@. Since formulae are essentially |
8 connectives @{text AX} and @{text EF}\@. Since formulae are essentially |
9 syntax trees, they are naturally modelled as a datatype:% |
9 syntax trees, they are naturally modelled as a datatype:% |
10 \footnote{The customary definition of PDL |
10 \footnote{The customary definition of PDL |
11 \cite{HarelKT-DL} looks quite different from ours, but the two are easily |
11 @{cite "HarelKT-DL"} looks quite different from ours, but the two are easily |
12 shown to be equivalent.} |
12 shown to be equivalent.} |
13 *} |
13 *} |
14 |
14 |
15 datatype formula = Atom "atom" |
15 datatype formula = Atom "atom" |
16 | Neg formula |
16 | Neg formula |