xDefine

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

Re-exported from bossLib.xDefine. See that entry for full documentation.