diff -r 039845fc96bd -r c9ff326e3ce5 CookBook/Package/Ind_General_Scheme.thy
--- a/CookBook/Package/Ind_General_Scheme.thy	Fri Feb 13 14:15:28 2009 +0000
+++ b/CookBook/Package/Ind_General_Scheme.thy	Sat Feb 14 00:11:50 2009 +0000
@@ -38,7 +38,7 @@
   \end{array}
   \]
 
-  The (weak) induction rules for the inductive predicates $R_1,\ldots,R_n$ are
+  The induction principles for the inductive predicates $R_1,\ldots,R_n$ are
 
   \[
   \begin{array}{l@ {\qquad}l}
@@ -62,8 +62,8 @@
   \]
 
   where $\vec{K}$ abbreviates $K_1,\ldots,K_r$. Applying the introduction rules for
-  $\forall$ and $\longrightarrow$ yields a proof state in which we have to prove $P_{l_i}~\vec{t}_i$
-  from the additional assumptions $\vec{K}$. When using $K_{l_i}$ (converted to meta-logic format)
+  $\forall$ and $\longrightarrow$ yields a goal state in which we have to prove $P_{l_i}~\vec{t}_i$
+  from the additional assumptions $\vec{K}$. When using $K_{l_i}$ (converted to the meta-logic format)
   to prove $P_{l_i}~\vec{t}_i$, we get subgoals $\vec{A}_i$ that are trivially solvable by assumption,
   as well as subgoals of the form
 
@@ -77,6 +77,8 @@
   \bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow
   \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{k_{ij}}~\vec{s}_{ij} \qquad \mbox{and} \qquad \vec{K}
   \]
+
+  What remains is to implement these proofs generically.
 *}
 
 end