--- a/ProgTutorial/Package/Ind_Intro.thy	Sun Apr 26 23:45:22 2009 +0200
+++ b/ProgTutorial/Package/Ind_Intro.thy	Wed Apr 29 00:36:14 2009 +0200
@@ -17,13 +17,13 @@
   \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
-  in terms of those constants, and the desired properties, for example
-  induction theorems or recursion equations, have to be derived from the definitions
+  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
   primitive operators of higher order logic, \emph{definitional packages} have
-  been implemented automating such work. Thanks to those packages, the user
+  been implemented to automate 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
@@ -32,11 +32,11 @@
   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
+  the basis of Isabelle/HOL's standard inductive definition package.  Instead, we
   will describe a simpler \emph{impredicative} (i.e.\ involving quantification on
   predicate variables) encoding of inductive predicates. Due to its
   simplicity, this package will necessarily have a reduced functionality. It
-  does neither support introduction rules involving arbitrary monotone
+  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.