Define

TotalDefn.Define : term quotation -> thm

General purpose function definition facility.

bossLib.Define is identical to TotalDefn.Define.

See also

bossLib.Define