Defn.Hol_defn

Hol_defn : string -> term quotation -> thm

STRUCTURE: Defn
SYNOPSIS: Function definition facility.
DESCRIPTION: bossLib.Hol_defn is identical to Defn.Hol_defn.
SEEALSO: Hol_defn

HOL Kananaskis-11