diff -r ee9d53fbb56b -r 24c68350d059 ProgTutorial/Package/Ind_Intro.thy
--- a/ProgTutorial/Package/Ind_Intro.thy	Thu Jul 30 11:38:52 2009 +0200
+++ b/ProgTutorial/Package/Ind_Intro.thy	Thu Jul 30 15:51:51 2009 +0200
@@ -5,23 +5,13 @@
 chapter {* How to Write a Definitional Package\label{chp:package} *}
 
 text {*
-  \begin{flushright}
-  {\em
-  ``My thesis is that programming is not at the bottom of the intellectual \\
-  pyramid, but at the top. It's creative design of the highest order. It \\
-  isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\
-  claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex]
-  Richard Bornat, In Defence of Programming \cite{Bornat-lecture}
-  \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
   in terms of those primitives, and the desired properties, for example
   induction theorems or recursion equations, are derived from the definitions
   by a formal proof. Since it would be very tedious for a user to define
-  complex inductive predicates or datatypes ``by hand'' just using the
+  inductive predicates or datatypes ``by hand'' just using the
   primitive operators of higher order logic, \emph{definitional packages} have
   been implemented to automate such work. Thanks to those packages, the user
   can give a high-level specification, for example a list of introduction
@@ -39,7 +29,8 @@
   does neither support introduction rules involving arbitrary monotonic
   operators, nor does it prove case analysis rules (also called inversion rules). 
   Moreover, it only proves a weaker form of the induction principle for inductive
-  predicates.
+  predicates. But it illustrates the implementation pf a typical package in
+  Isabelle.
 *}
 
 end