--- a/CookBook/Package/Ind_Intro.thy	Fri Feb 13 14:15:28 2009 +0000
+++ b/CookBook/Package/Ind_Intro.thy	Sat Feb 14 00:11:50 2009 +0000
@@ -11,23 +11,23 @@
   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}
+  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 constants, 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
-  primitive operators of higher order logic, packages have been implemented
-  automating such work. Thanks to those packages, the user can give a
-  high-level specification, like a list of introduction rules or constructors,
-  and the package then does all the low-level definitions and proofs behind
-  the scenes. In this chapter we explain how such a package can be
-  implemented.
+  implication, whose properties are described by axioms. All other concepts,
+  such as inductive predicates, datatypes, or recursive functions are defined
+  in terms of those constants, 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
+  primitive operators of higher order logic, \emph{definitional packages} have
+  been implemented automating such work. Thanks to those packages, the user
+  can give a high-level specification, for example a list of introduction
+  rules or constructors, and the package then does all the low-level
+  definitions and proofs behind the scenes. In this chapter we explain how
+  such a package can be implemented.
 
   As a running example, we have chosen a rather simple package for defining
   inductive predicates. To keep things really simple, we will not use the general
@@ -39,7 +39,7 @@
   have a reduced functionality. It does neither support introduction rules
   involving arbitrary monotone operators, nor does it prove case analysis (or
   inversion) rules. Moreover, it only proves a weaker form of the
-  induction theorem.
+  induction principle for inductive predicates.
 *}
 
 end