diff -r 780100cd4060 -r 1343540ed715 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Mon Nov 07 13:36:07 2011 +0000
+++ b/ProgTutorial/Tactical.thy	Mon Nov 07 16:13:26 2011 +0000
@@ -13,13 +13,6 @@
 chapter {* Tactical Reasoning\label{chp:tactical} *}
 
 text {*
-   \begin{flushright}
-  {\em ``The most effective debugging tool is still careful thought,\\ 
-  coupled with judiciously placed print statements.''} \\[1ex]
-  Brian Kernighan, in {\em Unix for Beginners}, 1979
-  \end{flushright}
-
-  \medskip
   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