--- a/ProgTutorial/Package/Ind_Interface.thy	Mon Mar 30 09:33:50 2009 +0100
+++ b/ProgTutorial/Package/Ind_Interface.thy	Tue Mar 31 15:48:53 2009 +0100
@@ -2,7 +2,7 @@
 imports "../Base" "../Parsing" Ind_Prelims Simple_Inductive_Package
 begin
 
-section {* Parsing and Typing the Specification *}
+section {* Parsing and Typing the Specification\label{sec:interface} *}
 
 text {* 
   To be able to write down the specification in Isabelle, we have to introduce
@@ -448,6 +448,11 @@
   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.
+
+  The code of the inductive package falls roughly in tree parts: the first
+  deals with the definitions, the second with the induction principles and 
+  the third with the introduction rules. 
+  
 *}