Hol_defn

Defn.Hol_defn : string -> term quotation -> defn

Function definition facility.

bossLib.Hol_defn is identical to Defn.Hol_defn.

See also

bossLib.Hol_defn