# HG changeset patch
# User nipkow
# Date 984649292 -3600
# Node ID 08188224c24e9d34f21de390d49f4a4180947e5c
# Parent  5bea3a8abdc3c1bd96af83977f8959679391b9ab
*** empty log message ***

diff -r 5bea3a8abdc3 -r 08188224c24e doc-src/TutorialI/CTL/PDL.thy
--- a/doc-src/TutorialI/CTL/PDL.thy	Wed Mar 14 18:40:01 2001 +0100
+++ b/doc-src/TutorialI/CTL/PDL.thy	Thu Mar 15 10:41:32 2001 +0100
@@ -3,8 +3,10 @@
 subsection{*Propositional Dynamic Logic --- PDL*}
 
 text{*\index{PDL|(}
-The formulae of PDL are built up from atomic propositions via the customary
-propositional connectives of negation and conjunction and the two temporal
+The formulae of PDL\footnote{The customary definition of PDL
+\cite{HarelKT-DL} looks quite different from ours, but the two are easily
+shown to be equivalent.} are built up from atomic propositions via
+negation and conjunction and the two temporal
 connectives @{text AX} and @{text EF}. Since formulae are essentially
 syntax trees, they are naturally modelled as a datatype:
 *}
diff -r 5bea3a8abdc3 -r 08188224c24e doc-src/TutorialI/CTL/document/PDL.tex
--- a/doc-src/TutorialI/CTL/document/PDL.tex	Wed Mar 14 18:40:01 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/PDL.tex	Thu Mar 15 10:41:32 2001 +0100
@@ -7,8 +7,10 @@
 %
 \begin{isamarkuptext}%
 \index{PDL|(}
-The formulae of PDL are built up from atomic propositions via the customary
-propositional connectives of negation and conjunction and the two temporal
+The formulae of PDL\footnote{The customary definition of PDL
+\cite{HarelKT-DL} looks quite different from ours, but the two are easily
+shown to be equivalent.} are built up from atomic propositions via
+negation and conjunction and the two temporal
 connectives \isa{AX} and \isa{EF}. Since formulae are essentially
 syntax trees, they are naturally modelled as a datatype:%
 \end{isamarkuptext}%
diff -r 5bea3a8abdc3 -r 08188224c24e doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Wed Mar 14 18:40:01 2001 +0100
+++ b/doc-src/TutorialI/tutorial.tex	Thu Mar 15 10:41:32 2001 +0100
@@ -89,7 +89,7 @@
 \input{Inductive/inductive}
 \input{Types/types}
 \input{Advanced/advanced}
-%\chapter{Theory Presentation}
+%\chapter{Theory Presentation} Document preparation / Syntax Matters!
 %\chapter{Case Study: Verifying a Cryptographic Protocol}
 %\chapter{Structured Proofs}
 %\label{ch:Isar}
diff -r 5bea3a8abdc3 -r 08188224c24e doc-src/manual.bib
--- a/doc-src/manual.bib	Wed Mar 14 18:40:01 2001 +0100
+++ b/doc-src/manual.bib	Thu Mar 15 10:41:32 2001 +0100
@@ -376,6 +376,9 @@
   publisher	= {Van Nostrand},
   year		= 1960}
 
+@book{HarelKT-DL,author={David Harel and Dexter Kozen and Jerzy Tiuryn},
+title={Dynamic Logic},publisher=MIT,year=2000}
+
 @Book{hennessy90,
   author	= {Matthew Hennessy},
   title		= {The Semantics of Programming Languages: An Elementary