--- 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.