--- a/ProgTutorial/First_Steps.thy	Mon Nov 07 13:36:07 2011 +0000
+++ b/ProgTutorial/First_Steps.thy	Mon Nov 07 16:13:26 2011 +0000
@@ -13,15 +13,10 @@
 chapter {* First Steps\label{chp:firststeps} *}
 
 text {*
-   \begin{flushright}
-  {\em
-  ``We will most likely never realize the full importance of painting the Tower,\\ 
-  that it is the essential element in the conservation of metal works and the\\ 
-  more meticulous the paint job, the longer the tower shall endure.''} \\[1ex]
-  Gustave Eiffel, in his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been 
-  re-painted 18 times since its initial construction, an average of once every 
-  seven years. It takes more than one year for a team of 25 painters to paint the tower 
-  from top to bottom.}
+  \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

--- a/ProgTutorial/Package/Ind_Intro.thy	Mon Nov 07 13:36:07 2011 +0000
+++ b/ProgTutorial/Package/Ind_Intro.thy	Mon Nov 07 16:13:26 2011 +0000
@@ -13,6 +13,18 @@
 chapter {* How to Write a Definitional Package\label{chp:package} *}
 
 text {*
+   \begin{flushright}
+  {\em
+  ``We will most likely never realize the full importance of painting the Tower,\\ 
+  that it is the essential element in the conservation of metal works and the\\ 
+  more meticulous the paint job, the longer the tower shall endure.''} \\[1ex]
+  Gustave Eiffel, in his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been 
+  re-painted 18 times since its initial construction, an average of once every 
+  seven years. It takes more than one year for a team of 25 painters to paint the tower 
+  from top to bottom.}
+  \end{flushright}
+
+  \medskip
   HOL is based on just a few primitive constants, like equality and
   implication, whose properties are described by axioms. All other concepts,
   such as inductive predicates, datatypes or recursive functions, are defined

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

Binary file progtutorial.pdf has changed