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