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