--- a/CookBook/Package/Ind_General_Scheme.thy	Sat Feb 14 16:09:04 2009 +0000
+++ b/CookBook/Package/Ind_General_Scheme.thy	Sun Feb 15 18:58:21 2009 +0000
@@ -7,11 +7,9 @@
 text {*
 
   Before we start with the implementation, it is useful to describe the general
-  form of inductive definitions that our package should accept. We closely follow
-  the notation for inductive definitions introduced by Schwichtenberg
-  \cite{Schwichtenberg-MLCF} for the Minlog system.
-  Let $R_1,\ldots,R_n$ be mutually inductive predicates and $\vec{p}$ be
-  parameters. Then the introduction rules for $R_1,\ldots,R_n$ may have
+  form of inductive definitions that our package should accept.
+  Suppose $R_1,\ldots,R_n$ be mutually inductive predicates and $\vec{p}$ be
+  some fixed parameters. Then the introduction rules for $R_1,\ldots,R_n$ may have
   the form
 
   \[
@@ -24,8 +22,8 @@
   Note that by disallowing the inductive predicates to occur in $\vec{B}_{ij}$ we make sure
   that all occurrences of the predicates in the premises of the introduction rules are
   \emph{strictly positive}. This condition guarantees the existence of predicates
-  that are closed under the introduction rules shown above. The inductive predicates
-  $R_1,\ldots,R_n$ can then be defined as follows:
+  that are closed under the introduction rules shown above. Then the definitions of the 
+  inductive predicates $R_1,\ldots,R_n$ is:
 
   \[
   \begin{array}{l@ {\qquad}l}