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