1\DOC WF_REL_TAC 2 3\TYPE {WF_REL_TAC : term quotation -> tactic} 4 5\SYNOPSIS 6Initiate a termination proof. 7 8\DESCRIBE 9{bossLib.WF_REL_TAC} is identical to {TotalDefn.WF_REL_TAC}. 10 11\SEEALSO 12bossLib.WF_REL_TAC. 13 14\ENDDOC 15