Hol_defn

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

Re-exported from bossLib.Hol_defn. See that entry for full documentation.