--- 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