structure IndDefRules
SYNOPSIS
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.
HOL  Trindemossen-1