HOL is based on just a few primitive constants, like equality and

  implication, whose properties are described by a few 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, packages have been implemented

  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.

  As a running example, we have chosen a rather simple package for defining

  inductive predicates. To keep things 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 will use a

  simpler \emph{impredicative} (i.e.\ involving quantification on predicate

  variables) encoding of inductive predicates suggested by Melham

  \cite{Melham:1992:PIR}. Due to its simplicity, this package will necessarily

  have a reduced functionality. It does neither support introduction rules

  involving arbitrary monotone operators, nor does it prove case analysis (or

  inversion) rules. Moreover, it only proves a weaker form of the rule

  induction theorem.