Define

TotalDefn.Define : term quotation -> thm

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