--- a/ProgTutorial/Intro.thy	Thu Jul 30 11:38:52 2009 +0200
+++ b/ProgTutorial/Intro.thy	Thu Jul 30 15:51:51 2009 +0200
@@ -5,6 +5,16 @@
 chapter {* Introduction *}
 
 text {*
+   \begin{flushright}
+  {\em
+  ``My thesis is that programming is not at the bottom of the intellectual \\
+  pyramid, but at the top. It's creative design of the highest order. It \\
+  isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\
+  claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex]
+  Richard Bornat, In Defence of Programming \cite{Bornat-lecture}
+  \end{flushright}
+
+  \medskip
   If your next project requires you to program on the ML-level of Isabelle,
   then this tutorial is for you. It will guide you through the first steps of
   Isabelle programming, and also explain tricks of the trade. The best way to
@@ -27,13 +37,11 @@
   Isabelle is implemented. If you are unfamiliar with either of these two
   subjects, you should first work through the Isabelle/HOL tutorial
   \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}.
-
 *}
 
 section {* Existing Documentation *}
 
 text {*
-  
   The following documentation about Isabelle programming already exists (and is
   part of the distribution of Isabelle):
 
@@ -68,14 +76,11 @@
   for Isabelle  provides convenient interfaces to query the history of
   files and ``change sets''.
   \end{description}
-
-
 *}
 
 section {* Typographic Conventions *}
 
 text {*
-
   All ML-code in this tutorial is typeset in shaded boxes, like the following 
   ML-expression:
 
@@ -160,7 +165,6 @@
   with checking agains the distribution, but generally problems will be caught
   and the developer, who caused them, is expected to fix them. So also
   in this case code maintenance is done for you. 
-
 *}
 
 section {* Some Naming Conventions in the Isabelle Sources *}
@@ -227,7 +231,6 @@
   chapters that are under \underline{heavy} construction are marked 
   with TBD.}
 
-  
   \vfill
   This document was compiled with:\\
   \input{version}\\