\DOC Hol_defn

\TYPE {Hol_defn : string -> term quotation -> defn}

\SYNOPSIS
Function definition facility.

\DESCRIBE
{bossLib.Hol_defn} is identical to {Defn.Hol_defn}.

\SEEALSO
bossLib.Hol_defn.

\ENDDOC