Tom Melham’s inference support for inductive definitions.
DESCRIPTION
IndDefRules provides support for reasoning about inductively
defined relations, including a general induction tactic, and an
entrypoint for deriving so-called ‘strong’ rule induction.