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.