1\DOC Hol_defn 2 3\TYPE {Hol_defn : string -> term quotation -> defn} 4 5\SYNOPSIS 6Function definition facility. 7 8\DESCRIBE 9{bossLib.Hol_defn} is identical to {Defn.Hol_defn}. 10 11\SEEALSO 12bossLib.Hol_defn. 13 14\ENDDOC 15