# HG changeset patch
# User nipkow
# Date 1407563955 -7200
# Node ID d02f0d44764846a0da032c5eb841a124ba473848
# Parent  51aa30c9ee4efa767cf04693750d55348296d7c1
tuned

diff -r 51aa30c9ee4e -r d02f0d447648 src/Doc/Prog_Prove/document/intro-isabelle.tex
--- a/src/Doc/Prog_Prove/document/intro-isabelle.tex	Fri Aug 08 17:36:08 2014 +0200
+++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex	Sat Aug 09 07:59:15 2014 +0200
@@ -82,13 +82,13 @@
 \emph{Programming and Proving in Isabelle/HOL} constitutes part~I of
 \href{http://www.in.tum.de/~nipkow/Concrete/}{Concrete Semantics}.  The web
 pages for \href{http://www.in.tum.de/~nipkow/Concrete/}{Concrete Semantics}
-also provide a set of \LaTeX-based slides for teaching \emph{Programming and
-Proving in Isabelle/HOL}.
+also provide a set of \LaTeX-based slides and Isabelle demo files
+for teaching \emph{Programming and Proving in Isabelle/HOL}.
 \fi
 
 \ifsem\else
 \paragraph{Acknowledgements}
 I wish to thank the following people for their comments on this document:
-Florian Haftmann, Ren\'{e} Thiemann, Sean Seefried, Christian Sternagel
-and Carl Witty.
+Florian Haftmann, Peter Johnson, Ren\'{e} Thiemann, Sean Seefried,
+Christian Sternagel and Carl Witty.
 \fi
\ No newline at end of file