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