diff -r 1aaa15ef731b -r 647cab4a72c2 ProgTutorial/Package/Ind_Prelims.thy
--- a/ProgTutorial/Package/Ind_Prelims.thy	Wed Apr 01 12:29:10 2009 +0100
+++ b/ProgTutorial/Package/Ind_Prelims.thy	Wed Apr 01 15:42:47 2009 +0100
@@ -27,7 +27,8 @@
   @{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}
   \end{center}
 
-  The package has to make an appropriate definition. Since an inductively
+  The package has to make an appropriate definition for @{term "trcl"}. 
+  Since an inductively
   defined predicate is the least predicate closed under a collection of
   introduction rules, the predicate @{text "trcl R x y"} can be defined so
   that it holds if and only if @{text "P x y"} holds for every predicate