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-10