33   inductive predicates. To keep things really simple, we will not use the general

    33   inductive predicates. To keep things really simple, we will not use the

    34   Knaster-Tarski fixpoint theorem on complete lattices, which forms the basis

    34   general Knaster-Tarski fixpoint theorem on complete lattices, which forms

    35   of Isabelle's standard inductive definition package.  Instead, we will use a

    35   the basis of Isabelle's standard inductive definition package.  Instead, we

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

    36   will use a simpler \emph{impredicative} (i.e.\ involving quantification on

    37   variables) encoding of inductive predicates suggested by Melham

    37   predicate variables) encoding of inductive predicates. Due to its

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

    38   simplicity, this package will necessarily have a reduced functionality. It

    39   have a reduced functionality. It does neither support introduction rules

    39   does neither support introduction rules involving arbitrary monotone

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

    40   operators, nor does it prove case analysis (or inversion) rules. Moreover,

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

    41   it only proves a weaker form of the induction principle for inductive

    42   induction principle for inductive predicates.

    42   predicates.