Hol_reln

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

Re-exported from bossLib.Hol_reln. See that entry for full documentation.