--- a/ProgTutorial/Package/Ind_Intro.thy	Tue Mar 31 20:31:18 2009 +0100
+++ b/ProgTutorial/Package/Ind_Intro.thy	Wed Apr 01 12:26:56 2009 +0100
@@ -17,9 +17,9 @@
   \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 have to be defined
+  such as inductive predicates, datatypes or recursive functions, have to be defined
   in terms of those constants, and the desired properties, for example
-  induction theorems, or recursion equations have to be derived from the definitions
+  induction theorems or recursion equations, have to be 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
@@ -29,7 +29,7 @@
   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
+  As the running example we have chosen a rather simple package for defining
   inductive predicates. To keep things really simple, we will not use the
   general Knaster-Tarski fixpoint theorem on complete lattices, which forms
   the basis of Isabelle's standard inductive definition package.  Instead, we