Hol_defn : string -> term quotation -> defn
STRUCTURE
SYNOPSIS
Function definition facility.
DESCRIPTION
bossLib.Hol_defn is identical to Defn.Hol_defn.
SEEALSO
HOL  Trindemossen-1