--- a/ProgTutorial/Advanced.thy	Sat Jan 21 15:16:04 2012 +0000
+++ b/ProgTutorial/Advanced.thy	Sat Jan 21 15:18:38 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	Sat Jan 21 15:16:04 2012 +0000
+++ b/ProgTutorial/Tactical.thy	Sat Jan 21 15:18:38 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