# HG changeset patch
# User nipkow
# Date 1334766256 -7200
# Node ID 2d49b0c9d8ec4173924ada90bda2bdaebf68ce52
# Parent  a2850a16e30f3a3a9d956c486f1b8d1f844f2d5d
tuned text, improved dependencies

diff -r a2850a16e30f -r 2d49b0c9d8ec doc-src/ProgProve/Makefile
--- 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
 
diff -r a2850a16e30f -r 2d49b0c9d8ec doc-src/ProgProve/intro-isabelle.tex
--- 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