xDefine

TotalDefn.xDefine : string -> term quotation -> thm

General purpose function definition facility.

bossLib.xDefine is identical to TotalDefn.xDefine.

See also

bossLib.xDefine