Define : term quotation -> thm
STRUCTURE
TotalDefn
SYNOPSIS
General purpose function definition facility.
DESCRIBE
bossLib.Define
is identical to
TotalDefn.Define
.
SEEALSO
Define
HOL
Kananaskis-4