diff -r fcc0e6e54dca -r 74846cb0fff9 CookBook/Package/Ind_Intro.thy
--- a/CookBook/Package/Ind_Intro.thy	Thu Feb 19 14:44:53 2009 +0000
+++ b/CookBook/Package/Ind_Intro.thy	Fri Feb 20 23:19:41 2009 +0000
@@ -30,16 +30,16 @@
   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
-  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
-  variables) encoding of inductive predicates suggested by Melham
-  \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
-  induction principle for inductive predicates.
+  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 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
+  predicates.
 *}
 
 end