--- a/ProgTutorial/Package/Ind_Intro.thy	Mon Mar 30 17:40:20 2009 +0200
+++ b/ProgTutorial/Package/Ind_Intro.thy	Wed Apr 01 12:28:14 2009 +0100
@@ -2,7 +2,7 @@
 imports Main 
 begin
 
-chapter {* How to Write a Definitional Package\label{chp:package} (TBD) *}
+chapter {* How to Write a Definitional Package\label{chp:package} *}
 
 text {*
   \begin{flushright}
@@ -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 have to be 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 have to be 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
@@ -29,7 +29,7 @@
   definitions and proofs behind the scenes. In this chapter we explain how
   such a package can be implemented.
 
-  As a running example, we have chosen a rather simple package for defining
+  As the running example we have chosen a rather simple package for defining
   inductive predicates. To keep things really simple, we will not use the
   general Knaster-Tarski fixpoint theorem on complete lattices, which forms
   the basis of Isabelle's standard inductive definition package.  Instead, we