diff -r fcc0e6e54dca -r 74846cb0fff9 CookBook/Package/Ind_General_Scheme.thy
--- a/CookBook/Package/Ind_General_Scheme.thy	Thu Feb 19 14:44:53 2009 +0000
+++ b/CookBook/Package/Ind_General_Scheme.thy	Fri Feb 20 23:19:41 2009 +0000
@@ -5,6 +5,11 @@
 section{* The General Construction Principle \label{sec:ind-general-method} *}
 
 text {*
+  
+  The point of these examples is to get a feeling what the automatic proofs 
+  should do in order to solve all inductive definitions we throw at them. For this 
+  it is instructive to look at the general construction principle 
+  of inductive definitions, which we shall do in the next section.
 
   Before we start with the implementation, it is useful to describe the general
   form of inductive definitions that our package should accept.