--- a/CookBook/Package/Ind_Intro.thy	Fri Feb 13 09:57:08 2009 +0000
+++ b/CookBook/Package/Ind_Intro.thy	Fri Feb 13 14:15:28 2009 +0000
@@ -16,7 +16,7 @@
 
   \medskip
   HOL is based on just a few primitive constants, like equality and
-  implication, whose properties are described by a few axioms. All other
+  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
@@ -30,7 +30,7 @@
   implemented.
 
   As a running example, we have chosen a rather simple package for defining
-  inductive predicates. To keep things simple, we will not use the general
+  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 will use a
   simpler \emph{impredicative} (i.e.\ involving quantification on predicate
@@ -38,7 +38,7 @@
   \cite{Melham:1992:PIR}. Due to its simplicity, this package will necessarily
   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 rule
+  inversion) rules. Moreover, it only proves a weaker form of the
   induction theorem.
 *}