doc-src/TutorialI/CTL/PDL.thy
changeset 18724 cb6e0064c88c
parent 17914 99ead7a7eb42
child 21202 6649bf75b9dc
equal deleted inserted replaced
18723:91d67d2f121c 18724:cb6e0064c88c
    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
    17                   | And formula formula
    17                   | And formula formula
    18                   | AX formula
    18                   | AX formula
    19                   | EF formula
    19                   | EF formula
    20 
    20