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