xDefine : string -> term quotation -> thm
STRUCTURE
TotalDefn
SYNOPSIS
General purpose function definition facility.
DESCRIPTION
bossLib.xDefine
is identical to
TotalDefn.xDefine
.
SEEALSO
xDefine
HOL
Kananaskis-11