Hol_defn : string -> term quotation -> thm
STRUCTURE
SYNOPSIS
Function definition facility.
DESCRIPTION
bossLib.Hol_defn is identical to Defn.Hol_defn.
SEEALSO
HOL  Kananaskis-10