--- a/ProgTutorial/Advanced.thy	Wed Nov 30 13:35:10 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Mon Jan 16 07:40:17 2012 +0000
@@ -32,7 +32,7 @@
   parallel.
 *}
 
-section {* Theories and Setups\label{sec:theories} *}
+section {* Theories\label{sec:theories} *}
 
 text {*
   Theories, as said above, are the most basic layer of abstraction in

--- a/ProgTutorial/Tactical.thy	Wed Nov 30 13:35:10 2011 +0000
+++ b/ProgTutorial/Tactical.thy	Mon Jan 16 07:40:17 2012 +0000
@@ -13,6 +13,19 @@
 chapter {* Tactical Reasoning\label{chp:tactical} *}
 
 text {*
+   \begin{flushright}
+  {\em
+  ``The first thing I would say is that when you write a program, think of\\ 
+   it primarily as a work of literature. You're trying to write something\\ 
+   that human beings are going to read. Don't think of it primarily as\\  
+   something a computer is going to follow. The more effective you are\\ 
+   at making your program readable, the more effective it's going to\\  
+   be: You'll understand it today, you'll understand it next week, and\\ 
+   your successors who are going to maintain and modify it will\\ 
+   understand it.''}\\[1ex]
+  Donald E.~Knuth, from an interview in Dr.~Dobb's Journal, 1996.
+  \end{flushright}
+
   One of the main reason for descending to the ML-level of Isabelle is to be
   able to implement automatic proof procedures. Such proof procedures can
   considerably lessen the burden of manual reasoning. They are centred around

Binary file progtutorial.pdf has changed