tuned
authornipkow
Sat, 09 Aug 2014 07:59:15 +0200
changeset 57819 d02f0d447648
parent 57818 51aa30c9ee4e
child 57820 b510819d58ee
tuned
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