Hol_reln : term quotation -> thm * thm * thm
STRUCTURE
SYNOPSIS
Definition facility for inductive predicates.
DESCRIPTION
bossLib.Hol_reln is identical to IndDefLib.Hol_reln.
SEEALSO
HOL  Trindemossen-1