1.1 --- a/doc-src/TutorialI/CTL/PDL.thy	Wed Mar 14 18:40:01 2001 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/PDL.thy	Thu Mar 15 10:41:32 2001 +0100
     1.3 @@ -3,8 +3,10 @@
     1.4  subsection{*Propositional Dynamic Logic --- PDL*}
     1.5  
     1.6  text{*\index{PDL|(}
     1.7 -The formulae of PDL are built up from atomic propositions via the customary
     1.8 -propositional connectives of negation and conjunction and the two temporal
     1.9 +The formulae of PDL\footnote{The customary definition of PDL
    1.10 +\cite{HarelKT-DL} looks quite different from ours, but the two are easily
    1.11 +shown to be equivalent.} are built up from atomic propositions via
    1.12 +negation and conjunction and the two temporal
    1.13  connectives @{text AX} and @{text EF}. Since formulae are essentially
    1.14  syntax trees, they are naturally modelled as a datatype:
    1.15  *}

     2.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex	Wed Mar 14 18:40:01 2001 +0100
     2.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex	Thu Mar 15 10:41:32 2001 +0100
     2.3 @@ -7,8 +7,10 @@
     2.4  %
     2.5  \begin{isamarkuptext}%
     2.6  \index{PDL|(}
     2.7 -The formulae of PDL are built up from atomic propositions via the customary
     2.8 -propositional connectives of negation and conjunction and the two temporal
     2.9 +The formulae of PDL\footnote{The customary definition of PDL
    2.10 +\cite{HarelKT-DL} looks quite different from ours, but the two are easily
    2.11 +shown to be equivalent.} are built up from atomic propositions via
    2.12 +negation and conjunction and the two temporal
    2.13  connectives \isa{AX} and \isa{EF}. Since formulae are essentially
    2.14  syntax trees, they are naturally modelled as a datatype:%
    2.15  \end{isamarkuptext}%

     3.1 --- a/doc-src/TutorialI/tutorial.tex	Wed Mar 14 18:40:01 2001 +0100
     3.2 +++ b/doc-src/TutorialI/tutorial.tex	Thu Mar 15 10:41:32 2001 +0100
     3.3 @@ -89,7 +89,7 @@
     3.4  \input{Inductive/inductive}
     3.5  \input{Types/types}
     3.6  \input{Advanced/advanced}
     3.7 -%\chapter{Theory Presentation}
     3.8 +%\chapter{Theory Presentation} Document preparation / Syntax Matters!
     3.9  %\chapter{Case Study: Verifying a Cryptographic Protocol}
    3.10  %\chapter{Structured Proofs}
    3.11  %\label{ch:Isar}

     4.1 --- a/doc-src/manual.bib	Wed Mar 14 18:40:01 2001 +0100
     4.2 +++ b/doc-src/manual.bib	Thu Mar 15 10:41:32 2001 +0100
     4.3 @@ -376,6 +376,9 @@
     4.4    publisher	= {Van Nostrand},
     4.5    year		= 1960}
     4.6  
     4.7 +@book{HarelKT-DL,author={David Harel and Dexter Kozen and Jerzy Tiuryn},
     4.8 +title={Dynamic Logic},publisher=MIT,year=2000}
     4.9 +
    4.10  @Book{hennessy90,
    4.11    author	= {Matthew Hennessy},
    4.12    title		= {The Semantics of Programming Languages: An Elementary