# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1326699617 0
# Node ID caa7331904544bbafb49da779a7089f6d212b1ea
# Parent  2862dacb04aa39cc41a6d9ea8bca0a23bc89f1f2
tuned

diff -r 2862dacb04aa -r caa733190454 ProgTutorial/Advanced.thy
--- 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
diff -r 2862dacb04aa -r caa733190454 ProgTutorial/Tactical.thy
--- 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
diff -r 2862dacb04aa -r caa733190454 progtutorial.pdf
Binary file progtutorial.pdf has changed