--- a/ProgTutorial/Package/Ind_Extensions.thy	Thu Apr 02 12:19:11 2009 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Fri Apr 03 07:55:07 2009 +0100
@@ -179,6 +179,13 @@
   Write code that automates the derivation of the strong induction 
   principles from the weak ones.
   \end{exercise}
+
+  \begin{readmore}
+  The standard inductive package is based on least fix-points. It allows more 
+  general introduction rules that can include any monotone operators and also
+  provides a richer reasoning infrastructure. The code of this package can be found in 
+  @{ML_file "HOL/Tools/inductive_package.ML"}.
+  \end{readmore}
 *}