diff -r b071a0b88298 -r 667a0943c40b CookBook/Package/Ind_Intro.thy
--- a/CookBook/Package/Ind_Intro.thy	Thu Jan 29 17:08:39 2009 +0000
+++ b/CookBook/Package/Ind_Intro.thy	Thu Jan 29 17:09:56 2009 +0000
@@ -15,20 +15,20 @@
   \end{flushright}
 
   \medskip
-  Higher order logic, as implemented in Isabelle/HOL, is based on just a few
-  primitive constants, like equality, implication, and the description
-  operator, whose properties are described as axioms. All other concepts, such
-  as inductive predicates, datatypes, or recursive functions are defined in
-  terms of those constants, and the desired properties, for example induction
-  theorems, or recursion equations are 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, Isabelle/HOL already contains a number of
-  packages automating such work. Thanks to those packages, the user can give a
-  high-level specification, like a list of introduction rules or constructors,
-  and the package then does all the low-level definitions and proofs behind
-  the scenes. In this chapter we explain how such a package can be
-  implemented.
+  HOL is based on just a few primitive constants, like equality, implication,
+  and the description operator, whose properties are described as axioms. All
+  other concepts, such as inductive predicates, datatypes, or recursive
+  functions are defined in terms of those constants, and the desired
+  properties, for example induction theorems, or recursion equations are
+  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,
+  Isabelle/HOL already contains a number of packages automating such
+  work. Thanks to those packages, the user can give a high-level
+  specification, like a list of introduction rules or constructors, and the
+  package then does all the low-level definitions and proofs behind the
+  scenes. In this chapter we explain how such a package can be implemented.
+
 
   %The packages are written in Standard ML, the implementation
   %language of Isabelle, and can be invoked by the user from within theory documents