--- a/ProgTutorial/Package/Ind_Intro.thy	Fri Mar 27 12:49:28 2009 +0000
+++ b/ProgTutorial/Package/Ind_Intro.thy	Fri Mar 27 18:19:42 2009 +0000
@@ -33,12 +33,12 @@
   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
+  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
-  operators, nor does it prove case analysis (or inversion) rules. Moreover,
-  it only proves a weaker form of the induction principle for inductive
+  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.
 *}