diff -r 780100cd4060 -r 1343540ed715 ProgTutorial/Package/Ind_Intro.thy --- 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