--- a/CookBook/Package/Ind_Intro.thy	Sat Feb 14 16:09:04 2009 +0000
+++ b/CookBook/Package/Ind_Intro.thy	Sun Feb 15 18:58:21 2009 +0000
@@ -17,9 +17,9 @@
   \medskip
   HOL is based on just a few primitive constants, like equality and
   implication, whose properties are described by axioms. All other concepts,
-  such as inductive predicates, datatypes, or recursive functions are defined
+  such as inductive predicates, datatypes, or recursive functions have to be defined
   in terms of those constants, and the desired properties, for example
-  induction theorems, or recursion equations are derived from the definitions
+  induction theorems, or recursion equations have to be derived from the definitions
   by a formal proof. Since it would be very tedious for a user to define
   complex inductive predicates or datatypes ``by hand'' just using the
   primitive operators of higher order logic, \emph{definitional packages} have