--- a/doc-src/ProgProve/Makefile Wed Apr 18 17:04:03 2012 +0200
+++ b/doc-src/ProgProve/Makefile Wed Apr 18 18:24:16 2012 +0200
@@ -9,8 +9,9 @@
NAME = prog-prove
-FILES = prog-prove.tex prog-prove.bib Thys/document/*.tex prelude.tex \
- svmono.cls mathpartir.sty isabelle.sty isabellesym.sty Thys/MyList.thy
+FILES = prog-prove.tex prog-prove.bib intro-isabelle.tex \
+ Thys/document/*.tex Thys/MyList.thy \
+ prelude.tex svmono.cls mathpartir.sty isabelle.sty isabellesym.sty
dvi: $(NAME).dvi
--- a/doc-src/ProgProve/intro-isabelle.tex Wed Apr 18 17:04:03 2012 +0200
+++ b/doc-src/ProgProve/intro-isabelle.tex Wed Apr 18 18:24:16 2012 +0200
@@ -35,4 +35,13 @@
For a comprehensive treatment of all things Isabelle we recommend the
\emph{Isabelle/Isar Reference Manual}~\cite{IsarRef}, which comes with the
Isabelle distribution.
-The tutorial by Nipkow, Paulson and Wenzel~\cite{LNCS2283} (in its updated version that comes with the Isabelle distribution) is still recommended for the wealth of examples and material, but its proof style is outdated. In particular it fails to cover the structured proof language Isar.
\ No newline at end of file
+The tutorial by Nipkow, Paulson and Wenzel~\cite{LNCS2283} (in its updated version that comes with the Isabelle distribution) is still recommended for the wealth of examples and material, but its proof style is outdated. In particular it fails to cover the structured proof language Isar.
+
+This introduction has grown out of many years of teaching Isabelle courses.
+It tries to cover the essentials (from a functional programming point of
+view) as quickly and compactly as possible. There is also an accompanying
+set of \LaTeX-based slides available from the author on request.
+
+\paragraph{Acknowledgements}
+I wish to thank the following people for their comments on this text:
+Florian Haftmann, Ren\'{e} Thiemann and Christian Sternagel.
\ No newline at end of file