--- a/ProgTutorial/Package/Ind_Interface.thy	Fri Mar 27 12:49:28 2009 +0000
+++ b/ProgTutorial/Package/Ind_Interface.thy	Fri Mar 27 18:19:42 2009 +0000
@@ -442,10 +442,12 @@
 *}
 
 text {*
-  From a high-level perspective the package consists of 6 subtasks:
+  (FIXME: perhaps move somewhere else)
 
-
-
+  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.
 *}