Hol_reln

IndDefLib.Hol_reln : term quotation -> thm * thm * thm

Definition facility for inductive predicates.

bossLib.Hol_reln is identical to IndDefLib.Hol_reln.

See also

bossLib.Hol_reln